![]() |
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 980 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) | |
2 | 3imp.1 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) | |
3 | 2 | imp31 256 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
4 | 1, 3 | sylbi 121 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∧ w3a 978 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 |
This theorem depends on definitions: df-bi 117 df-3an 980 |
This theorem is referenced by: 3impa 1194 3imp31 1196 3imp231 1197 3impb 1199 3impia 1200 3impib 1201 3com23 1209 3an1rs 1219 3imp1 1220 3impd 1221 syl3an2 1272 syl3an3 1273 3jao 1301 biimp3ar 1346 poxp 6235 tfrlemibxssdm 6330 tfr1onlembxssdm 6346 tfrcllembxssdm 6359 nndi 6489 nnmass 6490 pr2nelem 7192 xnn0lenn0nn0 9867 difelfzle 10136 fzo1fzo0n0 10185 elfzo0z 10186 fzofzim 10190 elfzodifsumelfzo 10203 mulexp 10561 expadd 10564 expmul 10567 bernneq 10643 facdiv 10720 dvdsaddre2b 11850 addmodlteqALT 11867 ltoddhalfle 11900 halfleoddlt 11901 dfgcd2 12017 cncongr1 12105 oddprmgt2 12136 prmfac1 12154 infpnlem1 12359 dfgrp3me 12975 mulgaddcom 13012 mulginvcom 13013 fiinopn 13589 opnneissb 13740 blssps 14012 blss 14013 2sqlem10 14557 |
Copyright terms: Public domain | W3C validator |