![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mp3an2 | Structured version Visualization version GIF version |
Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.) |
Ref | Expression |
---|---|
mp3an2.1 | ⊢ 𝜓 |
mp3an2.2 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
mp3an2 | ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp3an2.1 | . 2 ⊢ 𝜓 | |
2 | mp3an2.2 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
3 | 2 | 3expa 1098 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
4 | 1, 3 | mpanl2 688 | 1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 ∧ w3a 1068 |
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 199 df-an 388 df-3an 1070 |
This theorem is referenced by: mp3anl2 1435 tz7.7 6052 ordin 6056 onfr 6065 wfrlem14 7770 wfrlem17 7773 tfrlem11 7826 epfrs 8965 zorng 9722 tsk2 9983 tskcard 9999 gruina 10036 muladd11 10608 00id 10613 ltaddneg 10653 negsub 10733 subneg 10734 muleqadd 11083 diveq1 11130 conjmul 11156 recp1lt1 11337 nnsub 11482 addltmul 11681 nnunb 11701 zltp1le 11843 gtndiv 11870 eluzp1m1 12080 zbtwnre 12158 rebtwnz 12159 xnn0le2is012 12453 supxrbnd 12535 divelunit 12694 fznatpl1 12775 flbi2 13000 fldiv 13041 modid 13077 modm1p1mod0 13103 fzen2 13150 nn0ennn 13160 seqshft2 13209 seqf1olem1 13222 ser1const 13239 sq01 13399 expnbnd 13406 faclbnd3 13465 faclbnd5 13471 hashunsng 13564 hashunsngx 13565 hashxplem 13605 ccatrid 13748 sgnn 14312 sqrlem2 14462 sqrlem7 14467 leabs 14518 abs2dif 14551 cvgrat 15097 cos2t 15389 sin01gt0 15401 cos01gt0 15402 demoivre 15411 demoivreALT 15412 rpnnen2lem5 15429 rpnnen2lem12 15436 omeo 15573 gcd0id 15725 sqgcd 15763 isprm3 15881 eulerthlem2 15973 pczpre 16038 pcrec 16049 ressress 16416 mulgm1 18045 unitgrpid 19154 mdet0pr 20917 m2detleib 20956 cmpcov2 21714 ufileu 22243 tgpconncompeqg 22435 itg2ge0 24051 mdegldg 24375 abssinper 24821 ppiub 25494 chtub 25502 bposlem2 25575 lgs1 25631 colinearalglem4 26410 axsegconlem1 26418 axpaschlem 26441 axcontlem2 26466 axcontlem4 26468 axcontlem7 26471 axcontlem8 26472 funvtxval 26518 funiedgval 26519 vc0 28140 vcm 28142 nvmval2 28209 nvmf 28211 nvmdi 28214 nvnegneg 28215 nvpncan2 28219 nvaddsub4 28223 nvm1 28231 nvdif 28232 nvpi 28233 nvz0 28234 nvmtri 28237 nvabs 28238 nvge0 28239 imsmetlem 28256 4ipval2 28274 ipval3 28275 ipidsq 28276 dipcj 28280 sspmval 28299 ipasslem1 28397 ipasslem2 28398 dipsubdir 28414 hvsubdistr1 28617 shsubcl 28788 shsel3 28885 shunssi 28938 hosubdi 29378 lnopmi 29570 nmophmi 29601 nmopcoi 29665 opsqrlem6 29715 hstle 29800 hst0 29803 mdsl2i 29892 superpos 29924 dmdbr5ati 29992 f1rnen 30151 resvsca 30611 cvmliftphtlem 32178 topdifinffinlem 34099 finixpnum 34347 tan2h 34354 poimirlem3 34365 poimirlem4 34366 poimirlem7 34369 poimirlem16 34378 poimirlem17 34379 poimirlem19 34381 poimirlem20 34382 poimirlem24 34386 poimirlem28 34390 mblfinlem2 34400 mblfinlem4 34402 ismblfin 34403 el3v2 34966 atlatle 35930 pmaple 36371 dihglblem2N 37904 expgcd 38644 elnnrabdioph 38829 rabren3dioph 38837 zindbi 38968 expgrowth 40112 binomcxplemnotnn0 40133 trelpss 40235 etransc 42024 mogoldbb 43343 pgrple2abl 43804 aacllem 44294 |
Copyright terms: Public domain | W3C validator |