|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > mp4an | Structured version Visualization version GIF version | ||
| Description: An inference based on modus ponens. (Contributed by Jeff Madsen, 15-Jun-2010.) | 
| Ref | Expression | 
|---|---|
| mp4an.1 | ⊢ 𝜑 | 
| mp4an.2 | ⊢ 𝜓 | 
| mp4an.3 | ⊢ 𝜒 | 
| mp4an.4 | ⊢ 𝜃 | 
| mp4an.5 | ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏) | 
| Ref | Expression | 
|---|---|
| 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 692 | 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 207 df-an 396 | 
| This theorem is referenced by: noinfep 9701 1lt2nq 11014 m1p1sr 11133 m1m1sr 11134 axi2m1 11200 mul4i 11459 add4i 11487 add42i 11488 addsub4i 11606 muladdi 11715 lt2addi 11826 le2addi 11827 mulne0i 11907 divne0i 12016 divmuldivi 12028 divadddivi 12030 divdivdivi 12031 subreci 12099 8th4div3 12488 xrsup0 13366 fldiv4p1lem1div2 13876 sqrt2gt1lt2 15314 3dvds2dec 16371 flodddiv4 16453 nprmi 16727 mod2xnegi 17110 catcfuccl 18164 catcxpccl 18253 iccpnfhmeo 24977 xrhmeo 24978 cnheiborlem 24987 pcoval1 25047 pcoval2 25050 pcoass 25058 lhop1lem 26053 efcvx 26494 cos0pilt1 26575 dvrelog 26680 dvlog 26694 dvlog2 26696 dvsqrt 26785 dvcnsqrt 26787 cxpcn3 26792 ang180lem1 26853 dvatan 26979 log2cnv 26988 log2tlbnd 26989 log2ub 26993 harmonicbnd3 27052 ppiub 27249 bposlem8 27336 bposlem9 27337 lgsdir2lem1 27370 m1lgs 27433 2lgslem4 27451 2sqlem11 27474 2sqreultlem 27492 2sqreunnltlem 27495 chebbnd1 27517 0slt1s 27875 nohalf 28408 usgrexmplef 29277 siilem1 30871 hvadd4i 31078 his35i 31109 bdophsi 32116 bdopcoi 32118 mdcompli 32449 dmdcompli 32450 cshw1s2 32946 xrge00 33018 evl1deg3 33604 sqsscirc1 33908 raddcn 33929 xrge0iifcnv 33933 xrge0iifiso 33935 xrge0iifhom 33937 esumcvgsum 34090 dstfrvclim1 34481 signsply0 34567 cvmlift2lem6 35314 cvmlift2lem12 35320 iccioo01 37329 poimirlem9 37637 poimirlem15 37643 sqdeccom12 42329 lhe4.4ex1a 44353 dvcosre 45932 wallispi 46090 fourierdlem57 46183 fourierdlem58 46184 fourierdlem112 46238 fouriersw 46251 2exp340mod341 47725 8exp8mod9 47728 nfermltl8rev 47734 tgblthelfgott 47807 zlmodzxzequa 48418 zlmodzxzequap 48421 sepfsepc 48832 | 
| Copyright terms: Public domain | W3C validator |