![]() |
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 945 | . 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 943 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 |
This theorem depends on definitions: df-bi 116 df-3an 945 |
This theorem is referenced by: 3impa 1157 3impb 1158 3impia 1159 3impib 1160 3com23 1168 3an1rs 1178 3imp1 1179 3impd 1180 syl3an2 1231 syl3an3 1232 3jao 1260 biimp3ar 1305 poxp 6081 tfrlemibxssdm 6176 tfr1onlembxssdm 6192 tfrcllembxssdm 6205 nndi 6334 nnmass 6335 pr2nelem 6994 xnn0lenn0nn0 9535 difelfzle 9798 fzo1fzo0n0 9847 elfzo0z 9848 fzofzim 9852 elfzodifsumelfzo 9865 mulexp 10219 expadd 10222 expmul 10225 bernneq 10299 facdiv 10371 addmodlteqALT 11399 ltoddhalfle 11432 halfleoddlt 11433 dfgcd2 11542 cncongr1 11624 oddprmgt2 11654 prmfac1 11670 fiinopn 12008 opnneissb 12161 blssps 12410 blss 12411 |
Copyright terms: Public domain | W3C validator |