![]() |
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 710 | 1 ⊢ 𝜏 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
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 197 df-an 385 |
This theorem is referenced by: noinfep 8732 1lt2nq 10007 m1p1sr 10125 m1m1sr 10126 axi2m1 10192 mul4i 10445 add4i 10472 add42i 10473 addsub4i 10589 muladdi 10693 lt2addi 10802 le2addi 10803 mulne0i 10882 divne0i 10985 divmuldivi 10997 divadddivi 10999 divdivdivi 11000 subreci 11067 8th4div3 11464 xrsup0 12366 fldiv4p1lem1div2 12850 sqrt2gt1lt2 14234 3dvds2dec 15278 3dvds2decOLD 15279 flodddiv4 15359 nprmi 15624 mod2xnegi 15997 catcfuccl 16980 catcxpccl 17068 iccpnfhmeo 22965 xrhmeo 22966 cnheiborlem 22974 pcoval1 23033 pcoval2 23036 pcoass 23044 lhop1lem 23995 efcvx 24422 dvrelog 24603 dvlog 24617 dvlog2 24619 dvsqrt 24703 dvcnsqrt 24705 cxpcn3 24709 ang180lem1 24759 dvatan 24882 log2cnv 24891 log2tlbnd 24892 log2ub 24896 harmonicbnd3 24954 ppiub 25149 bposlem8 25236 bposlem9 25237 lgsdir2lem1 25270 m1lgs 25333 2lgslem4 25351 2sqlem11 25374 chebbnd1 25381 usgrexmplef 26371 siilem1 28036 hvadd4i 28245 his35i 28276 bdophsi 29285 bdopcoi 29287 mdcompli 29618 dmdcompli 29619 xrge00 30016 sqsscirc1 30284 raddcn 30305 xrge0iifcnv 30309 xrge0iifiso 30311 xrge0iifhom 30313 esumcvgsum 30480 dstfrvclim1 30869 signsply0 30958 cvmlift2lem6 31618 cvmlift2lem12 31624 poimirlem9 33749 poimirlem15 33755 lhe4.4ex1a 39048 dvcosre 40647 wallispi 40808 fourierdlem57 40901 fourierdlem58 40902 fourierdlem112 40956 fouriersw 40969 tgblthelfgott 42231 tgblthelfgottOLD 42237 zlmodzxzequa 42813 zlmodzxzequap 42816 |
Copyright terms: Public domain | W3C validator |