mp4an - Metamath Proof Explorer

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

Theorem mp4an 692

Description: An inference based on modus ponens. (Contributed by Jeff Madsen, 15-Jun-2010.)

**Hypotheses**
Ref	Expression
mp4an.1	⊢ 𝜑
mp4an.2	⊢ 𝜓
mp4an.3	⊢ 𝜒
mp4an.4	⊢ 𝜃
mp4an.5	⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)

**Assertion**
Ref	Expression
mp4an	⊢ 𝜏

**Proof of Theorem mp4an**
Step	Hyp	Ref	Expression
1		mp4an.1	. . 3 ⊢ 𝜑
2		mp4an.2	. . 3 ⊢ 𝜓
3	1, 2	pm3.2i 470	. 2 ⊢ (𝜑 ∧ 𝜓)
4		mp4an.3	. . 3 ⊢ 𝜒
5		mp4an.4	. . 3 ⊢ 𝜃
6	4, 5	pm3.2i 470	. 2 ⊢ (𝜒 ∧ 𝜃)
7		mp4an.5	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)
8	3, 6, 7	mp2an 691	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: noinfep 9683 1lt2nq 10996 m1p1sr 11115 m1m1sr 11116 axi2m1 11182 mul4i 11441 add4i 11468 add42i 11469 addsub4i 11586 muladdi 11695 lt2addi 11806 le2addi 11807 mulne0i 11887 divne0i 11992 divmuldivi 12004 divadddivi 12006 divdivdivi 12007 subreci 12074 8th4div3 12462 xrsup0 13334 fldiv4p1lem1div2 13832 sqrt2gt1lt2 15253 3dvds2dec 16309 flodddiv4 16389 nprmi 16659 mod2xnegi 17039 catcfuccl 18107 catcfucclOLD 18108 catcxpccl 18197 catcxpcclOLD 18198 iccpnfhmeo 24869 xrhmeo 24870 cnheiborlem 24879 pcoval1 24939 pcoval2 24942 pcoass 24950 lhop1lem 25945 efcvx 26385 cos0pilt1 26465 dvrelog 26570 dvlog 26584 dvlog2 26586 dvsqrt 26675 dvcnsqrt 26677 cxpcn3 26682 ang180lem1 26740 dvatan 26866 log2cnv 26875 log2tlbnd 26876 log2ub 26880 harmonicbnd3 26939 ppiub 27136 bposlem8 27223 bposlem9 27224 lgsdir2lem1 27257 m1lgs 27320 2lgslem4 27338 2sqlem11 27361 2sqreultlem 27379 2sqreunnltlem 27382 chebbnd1 27404 0slt1s 27761 usgrexmplef 29071 siilem1 30660 hvadd4i 30867 his35i 30898 bdophsi 31905 bdopcoi 31907 mdcompli 32238 dmdcompli 32239 cshw1s2 32681 xrge00 32742 sqsscirc1 33509 raddcn 33530 xrge0iifcnv 33534 xrge0iifiso 33536 xrge0iifhom 33538 esumcvgsum 33707 dstfrvclim1 34097 signsply0 34183 cvmlift2lem6 34918 cvmlift2lem12 34924 iccioo01 36806 poimirlem9 37102 poimirlem15 37108 sqdeccom12 41863 lhe4.4ex1a 43766 dvcosre 45300 wallispi 45458 fourierdlem57 45551 fourierdlem58 45552 fourierdlem112 45606 fouriersw 45619 2exp340mod341 47073 8exp8mod9 47076 nfermltl8rev 47082 tgblthelfgott 47155 zlmodzxzequa 47564 zlmodzxzequap 47567 sepfsepc 47946

W3C validator

	
		OSZAR »