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 1161 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜑 ∧ 𝜓 ∧ 𝜒)))) | |
2 | 3exp.1 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | syl8 71 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 963 |
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 965 |
This theorem is referenced by: 3expa 1185 3expb 1186 3expia 1187 3expib 1188 3com23 1191 3an1rs 1201 3exp1 1205 3expd 1206 exp5o 1208 syl3an2 1254 syl3an3 1255 syl2an23an 1281 3impexpbicomi 1419 rexlimdv3a 2576 rabssdv 3208 reupick2 3393 ssorduni 4446 tfisi 4546 fvssunirng 5483 f1oiso2 5777 poxp 6179 tfrlem5 6261 nndi 6433 nnmass 6434 findcard 6833 ac6sfi 6843 mulcanpig 7255 divgt0 8743 divge0 8744 uzind 9275 uzind2 9276 facavg 10620 prodfap0 11442 prodfrecap 11443 fprodabs 11513 dvdsmodexp 11691 dvdsnprmd 12002 prmndvdsfaclt 12031 fermltl 12109 fiinopn 12413 neipsm 12565 tpnei 12571 opnneiid 12575 neibl 12902 tgqioo 12958 |
Copyright terms: Public domain | W3C validator |