![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mp3an2 | 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 1139 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
4 | 1, 3 | mpanl2 426 | 1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ∧ w3a 920 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 df-3an 922 |
This theorem is referenced by: mp3anl2 1264 ordin 4176 ordsuc 4342 omv 6148 oeiv 6149 omv2 6158 1idprl 7052 muladd11 7518 negsub 7633 subneg 7634 ltaddneg 7805 muleqadd 8035 diveqap1 8070 conjmulap 8094 nnsub 8354 addltmul 8544 zltp1le 8700 gtndiv 8737 eluzp1m1 8937 divelunit 9314 fznatpl1 9383 flqbi2 9587 flqdiv 9617 frecfzen2 9723 nn0ennn 9729 iseqshft2 9767 faclbnd3 9986 shftfvalg 10080 ovshftex 10081 shftfval 10083 abs2dif 10366 omeo 10678 gcd0id 10750 sqgcd 10798 isprm3 10880 |
Copyright terms: Public domain | W3C validator |