![]() |
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 364 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | 3imp 1194 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∧ w3a 979 |
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 981 |
This theorem is referenced by: ex3 1196 3impdir 1304 syl3an9b 1320 biimp3a 1355 stoic3 1441 rspec3 2577 rspc3v 2869 raltpg 3657 rextpg 3658 disjiun 4010 otexg 4242 opelopabt 4274 tpexg 4456 3optocl 4716 fun2ssres 5271 funssfv 5553 fvun1 5595 foco2 5767 f1elima 5787 eloprabga 5975 caovimo 6082 ot1stg 6167 ot2ndg 6168 ot3rdgg 6169 brtposg 6269 rdgexggg 6392 rdgivallem 6396 nnmass 6502 nndir 6505 nnaword 6526 th3q 6654 ecovass 6658 ecoviass 6659 fpmg 6688 findcard 6902 unfiin 6939 addasspig 7343 mulasspig 7345 mulcanpig 7348 ltapig 7351 ltmpig 7352 addassnqg 7395 ltbtwnnqq 7428 mulnnnq0 7463 addassnq0 7475 genpassl 7537 genpassu 7538 genpassg 7539 aptiprleml 7652 adddir 7962 le2tri3i 8080 addsub12 8184 subdir 8357 reapmul1 8566 recexaplem2 8623 div12ap 8665 divdiv32ap 8691 divdivap1 8694 lble 8918 zaddcllemneg 9306 fnn0ind 9383 xrltso 9810 iccgelb 9946 elicc4 9954 elfz 10028 fzrevral 10119 expnegap0 10542 expgt0 10567 expge0 10570 expge1 10571 mulexpzap 10574 expp1zap 10583 expm1ap 10584 apexp1 10712 abssubap0 11113 binom 11506 dvds0lem 11822 dvdsnegb 11829 muldvds1 11837 muldvds2 11838 divalgmodcl 11947 gcd2n0cl 11984 lcmdvds 12093 prmdvdsexp 12162 rpexp1i 12168 eqglact 13125 lss0cl 13615 cnpval 14051 cnf2 14058 cnnei 14085 blssec 14291 blpnfctr 14292 mopni2 14336 mopni3 14337 |
Copyright terms: Public domain | W3C validator |