Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mp3an12 | GIF version |
Description: An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.) |
Ref | Expression |
---|---|
mp3an12.1 | ⊢ 𝜑 |
mp3an12.2 | ⊢ 𝜓 |
mp3an12.3 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
mp3an12 | ⊢ (𝜒 → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp3an12.2 | . 2 ⊢ 𝜓 | |
2 | mp3an12.1 | . . 3 ⊢ 𝜑 | |
3 | mp3an12.3 | . . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
4 | 2, 3 | mp3an1 1302 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃) |
5 | 1, 4 | mpan 420 | 1 ⊢ (𝜒 → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 962 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 964 |
This theorem is referenced by: mp3an12i 1319 ceqsralv 2712 brelrn 4767 funpr 5170 fpm 6568 ener 6666 ltaddnq 7208 ltadd1sr 7577 map2psrprg 7606 mul02 8142 ltapi 8391 div0ap 8455 divclapzi 8500 divcanap1zi 8501 divcanap2zi 8502 divrecapzi 8503 divcanap3zi 8504 divcanap4zi 8505 divassapzi 8515 divmulapzi 8516 divdirapzi 8517 redivclapzi 8531 ltm1 8597 mulgt1 8614 recgt1i 8649 recreclt 8651 ltmul1i 8671 ltdiv1i 8672 ltmuldivi 8673 ltmul2i 8674 lemul1i 8675 lemul2i 8676 cju 8712 nnge1 8736 nngt0 8738 nnrecgt0 8751 elnnnn0c 9015 elnnz1 9070 recnz 9137 eluzsubi 9346 ge0gtmnf 9599 m1expcl2 10308 1exp 10315 m1expeven 10333 expubnd 10343 iexpcyc 10390 expnbnd 10408 expnlbnd 10409 remim 10625 imval2 10659 cjdivapi 10700 absdivapzi 10919 ef01bndlem 11452 sin01gt0 11457 cos01gt0 11458 cos12dec 11463 absefib 11466 efieq1re 11467 zeo3 11554 evend2 11575 cnbl0 12692 sincosq1sgn 12896 sincosq3sgn 12898 sincosq4sgn 12899 |
Copyright terms: Public domain | W3C validator |