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 1171 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜑 ∧ 𝜓 ∧ 𝜒)))) | |
2 | 3exp.1 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | syl8 71 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 973 |
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 975 |
This theorem is referenced by: 3expa 1198 3expb 1199 3expia 1200 3expib 1201 3com23 1204 3an1rs 1214 3exp1 1218 3expd 1219 exp5o 1221 syl3an2 1267 syl3an3 1268 syl2an23an 1294 3impexpbicomi 1432 rexlimdv3a 2589 rabssdv 3227 reupick2 3413 ssorduni 4471 tfisi 4571 fvssunirng 5511 f1oiso2 5806 poxp 6211 tfrlem5 6293 nndi 6465 nnmass 6466 findcard 6866 ac6sfi 6876 mulcanpig 7297 divgt0 8788 divge0 8789 uzind 9323 uzind2 9324 facavg 10680 prodfap0 11508 prodfrecap 11509 fprodabs 11579 dvdsmodexp 11757 dvdsnprmd 12079 prmndvdsfaclt 12110 fermltl 12188 pceu 12249 fiinopn 12796 neipsm 12948 tpnei 12954 opnneiid 12958 neibl 13285 tgqioo 13341 |
Copyright terms: Public domain | W3C validator |