imdistani - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > imdistani		Structured version Visualization version GIF version

Theorem imdistani 568

Description: Distribution of implication with conjunction. (Contributed by NM, 1-Aug-1994.)

**Hypothesis**
Ref	Expression
imdistani.1	⊢ (𝜑 → (𝜓 → 𝜒))

**Assertion**
Ref	Expression
imdistani	⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜒))

**Proof of Theorem imdistani**
Step	Hyp	Ref	Expression
1		imdistani.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	anc2li 555	. 2 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜒)))
3	2	imp 406	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜒))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8

This theorem depends on definitions: df-bi 206 df-an 396

This theorem is referenced by: syldanl 601 cases2ALT 1047 reximia 3078 2reu1 3890 difrab 4309 rabsnifsb 4727 foconst 6826 elfvmptrab 7034 dffo4 7113 dffo5 7114 isofrlem 7348 brfvopab 7477 onint 7793 el2mpocl 8091 suppofssd 8209 tz7.48lem 8462 opthreg 9642 eltsk2g 10775 recgt1i 12142 sup2 12201 elnnnn0c 12548 elnnz1 12619 recnz 12668 eluz2b2 12936 iccsplit 13495 elfzp12 13613 1mod 13901 pfxsuff1eqwrdeq 14682 cos01gt0 16168 oddnn02np1 16325 reumodprminv 16773 clatl 18500 isacs4lem 18536 isacs5lem 18537 isnzr2hash 20458 c0rnghm 20472 isdomn4 21250 mplcoe5lem 21977 ioovolcl 25512 elply2 26143 cusgrsize 29281 rusgrpropedg 29411 wlkonprop 29485 wksonproplem 29531 wksonproplemOLD 29532 pthdlem1 29593 3oalem1 31485 elorrvc 34083 ballotlemfc0 34112 ballotlemfcc 34113 ballotlemodife 34117 ballotth 34157 nummin 34714 opnrebl2 35805 bj-eldiag2 36656 topdifinffinlem 36826 finxpsuc 36877 wl-ax11-lem3 37054 matunitlindflem2 37090 matunitlindf 37091 poimirlem28 37121 poimirlem29 37122 mblfinlem1 37130 ovoliunnfl 37135 voliunnfl 37137 itg2addnclem2 37145 areacirclem5 37185 seqpo 37220 incsequz 37221 incsequz2 37222 ismtycnv 37275 prnc 37540 dihatexv2 40812 sn-sup2 42024 prjspval 42027 tfsconcatlem 42765 omssrncard 42970 reabsifneg 43062 reabsifnpos 43063 reabsifpos 43064 reabsifnneg 43065 fperiodmullem 44685 climsuselem1 44995 climsuse 44996 0ellimcdiv 45037 fperdvper 45307 iblsplit 45354 stirlinglem11 45472 qndenserrnbllem 45682 sge0fodjrnlem 45804 upwlkbprop 47200 regt1loggt0 47609

	
		OSZAR »