Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3imp | GIF version |
Description: Importation inference. (Contributed by NM, 8-Apr-1994.) |
Ref | Expression |
---|---|
3imp.1 | ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
Ref | Expression |
---|---|
3imp | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-3an 965 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) | |
2 | 3imp.1 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) | |
3 | 2 | imp31 254 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
4 | 1, 3 | sylbi 120 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 963 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 |
This theorem depends on definitions: df-bi 116 df-3an 965 |
This theorem is referenced by: 3impa 1177 3imp31 1178 3imp231 1179 3impb 1181 3impia 1182 3impib 1183 3com23 1191 3an1rs 1201 3imp1 1202 3impd 1203 syl3an2 1254 syl3an3 1255 3jao 1283 biimp3ar 1328 poxp 6180 tfrlemibxssdm 6275 tfr1onlembxssdm 6291 tfrcllembxssdm 6304 nndi 6434 nnmass 6435 pr2nelem 7127 xnn0lenn0nn0 9770 difelfzle 10037 fzo1fzo0n0 10086 elfzo0z 10087 fzofzim 10091 elfzodifsumelfzo 10104 mulexp 10462 expadd 10465 expmul 10468 bernneq 10542 facdiv 10616 addmodlteqALT 11755 ltoddhalfle 11788 halfleoddlt 11789 dfgcd2 11902 cncongr1 11984 oddprmgt2 12015 prmfac1 12031 fiinopn 12444 opnneissb 12597 blssps 12869 blss 12870 |
Copyright terms: Public domain | W3C validator |