Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3exp | GIF version |
Description: Exportation inference. (Contributed by NM, 30-May-1994.) |
Ref | Expression |
---|---|
3exp.1 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
3exp | ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm3.2an3 1145 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜑 ∧ 𝜓 ∧ 𝜒)))) | |
2 | 3exp.1 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | syl8 71 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 947 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 949 |
This theorem is referenced by: 3expa 1166 3expb 1167 3expia 1168 3expib 1169 3com23 1172 3an1rs 1182 3exp1 1186 3expd 1187 exp5o 1189 syl3an2 1235 syl3an3 1236 syl2an23an 1262 3impexpbicomi 1400 rexlimdv3a 2528 rabssdv 3147 reupick2 3332 ssorduni 4373 tfisi 4471 fvssunirng 5404 f1oiso2 5696 poxp 6097 tfrlem5 6179 nndi 6350 nnmass 6351 findcard 6750 ac6sfi 6760 mulcanpig 7111 divgt0 8598 divge0 8599 uzind 9130 uzind2 9131 facavg 10460 dvdsnprmd 11733 prmndvdsfaclt 11761 fiinopn 12098 neipsm 12250 tpnei 12256 opnneiid 12260 neibl 12587 tgqioo 12643 |
Copyright terms: Public domain | W3C validator |