![]() |
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 1118 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜑 ∧ 𝜓 ∧ 𝜒)))) | |
2 | 3exp.1 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | syl8 70 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 920 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 df-3an 922 |
This theorem is referenced by: 3expa 1139 3expb 1140 3expia 1141 3expib 1142 3com23 1145 3an1rs 1151 3exp1 1155 3expd 1156 exp5o 1158 syl3an2 1204 syl3an3 1205 syl2an23an 1231 3impexpbicomi 1369 rexlimdv3a 2484 rabssdv 3083 reupick2 3266 ssorduni 4259 tfisi 4356 fvssunirng 5241 f1oiso2 5517 poxp 5904 tfrlem5 5983 nndi 6150 nnmass 6151 findcard 6444 ac6sfi 6454 mulcanpig 6639 divgt0 8069 divge0 8070 uzind 8591 uzind2 8592 facavg 9822 dvdsnprmd 10714 prmndvdsfaclt 10742 |
Copyright terms: Public domain | W3C validator |