| 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 1202 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜑 ∧ 𝜓 ∧ 𝜒)))) | |
| 2 | 3exp.1 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
| 3 | 1, 2 | syl8 71 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 ∧ w3a 1004 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
| This theorem depends on definitions: df-bi 117 df-3an 1006 |
| This theorem is referenced by: 3expa 1229 3expb 1230 3expia 1231 3expib 1232 3com23 1235 3an1rs 1245 3exp1 1249 3expd 1250 exp5o 1252 syl3an2 1307 syl3an3 1308 syl2an23an 1335 3impexpbicomi 1484 rexlimdv3a 2652 rabssdv 3307 reupick2 3493 ssorduni 4585 tfisi 4685 fvssunirng 5654 f1oiso2 5968 poxp 6397 tfrlem5 6480 nndi 6654 nnmass 6655 findcard 7077 ac6sfi 7087 mulcanpig 7555 divgt0 9052 divge0 9053 uzind 9591 uzind2 9592 facavg 11009 prodfap0 12111 prodfrecap 12112 fprodabs 12182 dvdsmodexp 12361 dvdsaddre2b 12407 dvdsnprmd 12702 prmndvdsfaclt 12733 fermltl 12811 pceu 12873 mulgass2 14077 islss4 14402 rnglidlmcl 14500 fiinopn 14734 neipsm 14884 tpnei 14890 opnneiid 14894 neibl 15221 tgqioo 15285 gausslemma2dlem1a 15793 ausgrumgrien 16027 ausgrusgrien 16028 usgrausgrben 16029 ushgredgedg 16083 ushgredgedgloop 16085 wlkl1loop 16215 |
| Copyright terms: Public domain | W3C validator |