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 1441 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
5 | 1, 4 | mpan 686 | 1 ⊢ (𝜓 → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1079 |
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 df-3an 1081 |
This theorem is referenced by: predeq2 6144 wrecseq2 7940 oeoalem 8211 mulid1 10627 addltmul 11861 eluzaddi 12259 fz01en 12923 fznatpl1 12949 expubnd 13529 bernneq 13578 bernneq2 13579 faclbnd4lem1 13641 hashfun 13786 bpoly2 15399 bpoly3 15400 fsumcube 15402 efi4p 15478 efival 15493 cos2tsin 15520 cos01bnd 15527 cos01gt0 15532 dvds0 15613 odd2np1 15678 opoe 15700 divalglem0 15732 gcdid 15863 pythagtriplem4 16144 ressid 16547 fvpr0o 16820 fvpr1o 16821 zringcyg 20566 lecldbas 21755 blssioo 23330 tgioo 23331 rerest 23339 xrrest 23342 zdis 23351 reconnlem2 23362 metdscn2 23392 negcncf 23453 iihalf2 23464 cncmet 23852 rrxmvallem 23934 rrxmval 23935 ovolunlem1a 24024 ismbf3d 24182 c1lip2 24522 pilem2 24967 pilem3 24968 sinperlem 24993 sincosq1sgn 25011 sincosq2sgn 25012 sinq12gt0 25020 cosq14gt0 25023 cosq14ge0 25024 coseq1 25037 sinord 25045 zetacvg 25519 1sgmprm 25702 ppiub 25707 chtublem 25714 chtub 25715 bcp1ctr 25782 bpos1lem 25785 bposlem2 25788 bposlem3 25789 bposlem4 25790 bposlem5 25791 bposlem6 25792 bposlem7 25793 bposlem9 25795 axlowdim 26674 ipidsq 28414 ipasslem1 28535 ipasslem2 28536 ipasslem4 28538 ipasslem5 28539 ipasslem8 28541 ipasslem9 28542 ipasslem11 28544 pjoc1i 29135 h1de2bi 29258 h1de2ctlem 29259 spanunsni 29283 opsqrlem1 29844 opsqrlem6 29849 chrelati 30068 chrelat2i 30069 cvexchlem 30072 pnfinf 30739 rrhre 31161 erdszelem5 32339 wsuceq2 33000 taupilem1 34484 finxpreclem2 34553 sin2h 34763 cos2h 34764 tan2h 34765 poimirlem27 34800 poimirlem30 34803 broucube 34807 mblfinlem1 34810 heiborlem6 34975 icccncfext 42046 dirkertrigeq 42263 zlmodzxzel 44331 dignn0flhalflem1 44603 fv1prop 44614 fv2prop 44615 line2x 44669 onetansqsecsq 44788 cotsqcscsq 44789 |
Copyright terms: Public domain | W3C validator |