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 975 | . 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 973 |
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 975 |
This theorem is referenced by: 3impa 1189 3imp31 1191 3imp231 1192 3impb 1194 3impia 1195 3impib 1196 3com23 1204 3an1rs 1214 3imp1 1215 3impd 1216 syl3an2 1267 syl3an3 1268 3jao 1296 biimp3ar 1341 poxp 6211 tfrlemibxssdm 6306 tfr1onlembxssdm 6322 tfrcllembxssdm 6335 nndi 6465 nnmass 6466 pr2nelem 7168 xnn0lenn0nn0 9822 difelfzle 10090 fzo1fzo0n0 10139 elfzo0z 10140 fzofzim 10144 elfzodifsumelfzo 10157 mulexp 10515 expadd 10518 expmul 10521 bernneq 10596 facdiv 10672 addmodlteqALT 11819 ltoddhalfle 11852 halfleoddlt 11853 dfgcd2 11969 cncongr1 12057 oddprmgt2 12088 prmfac1 12106 infpnlem1 12311 fiinopn 12796 opnneissb 12949 blssps 13221 blss 13222 2sqlem10 13755 |
Copyright terms: Public domain | W3C validator |