![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3impa | GIF version |
Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.) |
Ref | Expression |
---|---|
3impa.1 | ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
3impa | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3impa.1 | . . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
2 | 1 | exp31 359 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | 3imp 1158 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 945 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 947 |
This theorem is referenced by: 3impdir 1255 syl3an9b 1271 biimp3a 1306 stoic3 1390 rspec3 2496 rspc3v 2775 raltpg 3542 rextpg 3543 disjiun 3890 otexg 4112 opelopabt 4144 tpexg 4325 3optocl 4577 fun2ssres 5124 funssfv 5401 fvun1 5441 foco2 5609 f1elima 5628 eloprabga 5812 caovimo 5918 ot1stg 6004 ot2ndg 6005 ot3rdgg 6006 brtposg 6105 rdgexggg 6228 rdgivallem 6232 nnmass 6337 nndir 6340 nnaword 6361 th3q 6488 ecovass 6492 ecoviass 6493 fpmg 6522 findcard 6735 unfiin 6767 addasspig 7086 mulasspig 7088 mulcanpig 7091 ltapig 7094 ltmpig 7095 addassnqg 7138 ltbtwnnqq 7171 mulnnnq0 7206 addassnq0 7218 genpassl 7280 genpassu 7281 genpassg 7282 aptiprleml 7395 adddir 7681 le2tri3i 7795 addsub12 7898 subdir 8067 reapmul1 8275 recexaplem2 8326 div12ap 8367 divdiv32ap 8393 divdivap1 8396 lble 8615 zaddcllemneg 8997 fnn0ind 9071 xrltso 9475 iccgelb 9608 elicc4 9616 elfz 9689 fzrevral 9778 expnegap0 10194 expgt0 10219 expge0 10222 expge1 10223 mulexpzap 10226 expp1zap 10235 expm1ap 10236 abssubap0 10754 binom 11145 dvds0lem 11351 dvdsnegb 11358 muldvds1 11366 muldvds2 11367 divalgmodcl 11473 gcd2n0cl 11506 lcmdvds 11606 prmdvdsexp 11672 rpexp1i 11678 cnpval 12209 cnf2 12216 cnnei 12243 blssec 12427 blpnfctr 12428 mopni2 12472 mopni3 12473 |
Copyright terms: Public domain | W3C validator |