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 471 | . 2 ⊢ (𝜑 ∧ 𝜓) |
4 | mp4an.3 | . . 3 ⊢ 𝜒 | |
5 | mp4an.4 | . . 3 ⊢ 𝜃 | |
6 | 4, 5 | pm3.2i 471 | . 2 ⊢ (𝜒 ∧ 𝜃) |
7 | mp4an.5 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏) | |
8 | 3, 6, 7 | mp2an 688 | 1 ⊢ 𝜏 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: noinfep 9112 1lt2nq 10384 m1p1sr 10503 m1m1sr 10504 axi2m1 10570 mul4i 10826 add4i 10853 add42i 10854 addsub4i 10971 muladdi 11080 lt2addi 11191 le2addi 11192 mulne0i 11272 divne0i 11377 divmuldivi 11389 divadddivi 11391 divdivdivi 11392 subreci 11459 8th4div3 11846 xrsup0 12706 fldiv4p1lem1div2 13195 sqrt2gt1lt2 14624 3dvds2dec 15672 flodddiv4 15754 nprmi 16023 mod2xnegi 16397 catcfuccl 17359 catcxpccl 17447 iccpnfhmeo 23478 xrhmeo 23479 cnheiborlem 23487 pcoval1 23546 pcoval2 23549 pcoass 23557 lhop1lem 24539 efcvx 24966 dvrelog 25147 dvlog 25161 dvlog2 25163 dvsqrt 25250 dvcnsqrt 25252 cxpcn3 25256 ang180lem1 25314 dvatan 25440 log2cnv 25450 log2tlbnd 25451 log2ub 25455 harmonicbnd3 25513 ppiub 25708 bposlem8 25795 bposlem9 25796 lgsdir2lem1 25829 m1lgs 25892 2lgslem4 25910 2sqlem11 25933 2sqreultlem 25951 2sqreunnltlem 25954 chebbnd1 25976 usgrexmplef 26969 siilem1 28556 hvadd4i 28763 his35i 28794 bdophsi 29801 bdopcoi 29803 mdcompli 30134 dmdcompli 30135 cshw1s2 30562 xrge00 30601 sqsscirc1 31051 raddcn 31072 xrge0iifcnv 31076 xrge0iifiso 31078 xrge0iifhom 31080 esumcvgsum 31247 dstfrvclim1 31635 signsply0 31721 cvmlift2lem6 32453 cvmlift2lem12 32459 poimirlem9 34783 poimirlem15 34789 sqdeccom12 39055 lhe4.4ex1a 40541 dvcosre 42076 wallispi 42236 fourierdlem57 42329 fourierdlem58 42330 fourierdlem112 42384 fouriersw 42397 2exp340mod341 43745 8exp8mod9 43748 nfermltl8rev 43754 tgblthelfgott 43827 zlmodzxzequa 44449 zlmodzxzequap 44452 |
Copyright terms: Public domain | W3C validator |