![]() |
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 346 | . 2 ⊢ (φ → (ψ → (χ → θ))) |
3 | 2 | 3imp 1097 | 1 ⊢ ((φ ∧ ψ ∧ χ) → θ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 ∧ w3a 884 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 df-3an 886 |
This theorem is referenced by: 3impdir 1190 syl3an9b 1204 biimp3a 1234 stoic3 1317 rspec3 2403 rspc3v 2659 raltpg 3414 rextpg 3415 otexg 3958 opelopabt 3990 tpexg 4145 3optocl 4361 fun2ssres 4886 funssfv 5142 fvun1 5182 foco2 5261 f1elima 5355 eloprabga 5533 caovimo 5636 ot1stg 5721 ot2ndg 5722 ot3rdgg 5723 brtposg 5810 rdgexggg 5904 rdgivallem 5908 frecsuclem1 5926 nnmass 6005 nndir 6008 nnaword 6020 th3q 6147 ecovass 6151 ecoviass 6152 addasspig 6314 mulasspig 6316 mulcanpig 6319 ltapig 6322 ltmpig 6323 addassnqg 6366 ltbtwnnqq 6398 mulnnnq0 6433 addassnq0 6445 genpassl 6507 genpassu 6508 genpassg 6509 aptiprleml 6611 adddir 6816 le2tri3i 6923 addsub12 7021 subdir 7179 reapmul1 7379 recexaplem2 7415 div12ap 7455 divdiv32ap 7478 divdivap1 7481 zaddcllemneg 8060 fnn0ind 8130 xrltso 8487 iccgelb 8571 elicc4 8579 elfz 8650 fzrevral 8737 expivallem 8910 expnegap0 8917 expgt0 8942 expge0 8945 expge1 8946 mulexpzap 8949 expp1zap 8957 expm1ap 8958 |
Copyright terms: Public domain | W3C validator |