| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > mp3an13 | Structured version Visualization version GIF version | ||
| Description: An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.) |
| Ref | Expression |
|---|---|
| mp3an13.1 | ⊢ 𝜑 |
| mp3an13.2 | ⊢ 𝜒 |
| mp3an13.3 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
| Ref | Expression |
|---|---|
| mp3an13 | ⊢ (𝜓 → 𝜃) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mp3an13.1 | . 2 ⊢ 𝜑 | |
| 2 | mp3an13.2 | . . 3 ⊢ 𝜒 | |
| 3 | mp3an13.3 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
| 4 | 2, 3 | mp3an3 1452 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
| 5 | 1, 4 | mpan 690 | 1 ⊢ (𝜓 → 𝜃) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ w3a 1087 |
| 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 df-3an 1089 |
| This theorem is referenced by: predeq2 6324 wrecseq2 8344 oeoalem 8634 mulrid 11259 addltmul 12502 eluzaddiOLD 12910 fz01en 13592 fznatpl1 13618 expubnd 14217 bernneq 14268 bernneq2 14269 faclbnd4lem1 14332 hashfun 14476 bpoly2 16093 bpoly3 16094 fsumcube 16096 efi4p 16173 efival 16188 cos2tsin 16215 cos01bnd 16222 cos01gt0 16227 dvds0 16309 odd2np1 16378 opoe 16400 divalglem0 16430 gcdid 16564 pythagtriplem4 16857 ressid 17290 fvpr0o 17604 fvpr1o 17605 zringcyg 21480 lecldbas 23227 blssioo 24816 tgioo 24817 rerest 24825 xrrest 24829 zdis 24838 reconnlem2 24849 metdscn2 24879 negcncf 24948 negcncfOLD 24949 iihalf2 24961 cncmet 25356 rrxmvallem 25438 rrxmval 25439 ovolunlem1a 25531 ismbf3d 25689 c1lip2 26037 pilem2 26496 pilem3 26497 sinperlem 26522 sincosq1sgn 26540 sincosq2sgn 26541 sinq12gt0 26549 cosq14gt0 26552 cosq14ge0 26553 coseq1 26567 sinord 26576 zetacvg 27058 1sgmprm 27243 ppiub 27248 chtublem 27255 chtub 27256 bcp1ctr 27323 bpos1lem 27326 bposlem2 27329 bposlem3 27330 bposlem4 27331 bposlem5 27332 bposlem6 27333 bposlem7 27334 bposlem9 27336 nnsge1 28346 cutpw2 28417 pw2bday 28418 pw2cut 28420 zs12bday 28424 axlowdim 28976 ipidsq 30729 ipasslem1 30850 ipasslem2 30851 ipasslem4 30853 ipasslem5 30854 ipasslem8 30856 ipasslem9 30857 ipasslem11 30859 pjoc1i 31450 h1de2bi 31573 h1de2ctlem 31574 spanunsni 31598 opsqrlem1 32159 opsqrlem6 32164 chrelati 32383 chrelat2i 32384 cvexchlem 32387 pnfinf 33190 1fldgenq 33324 rrhre 34022 erdszelem5 35200 wsuceq2 35817 taupilem1 37322 finxpreclem2 37391 sin2h 37617 cos2h 37618 tan2h 37619 poimirlem27 37654 poimirlem30 37657 broucube 37661 mblfinlem1 37664 heiborlem6 37823 lcmineqlem19 42048 2xp3dxp2ge1d 42242 onexomgt 43253 omabs2 43345 icccncfext 45902 dirkertrigeq 46116 zlmodzxzel 48271 dignn0flhalflem1 48536 2arymaptfo 48575 fv1prop 48620 fv2prop 48621 line2x 48675 onetansqsecsq 49280 cotsqcscsq 49281 |
| Copyright terms: Public domain | W3C validator |