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 1098 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 ∧ w3a 885 |
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 887 |
This theorem is referenced by: 3impdir 1191 syl3an9b 1205 biimp3a 1235 stoic3 1320 rspec3 2409 rspc3v 2665 raltpg 3423 rextpg 3424 otexg 3967 opelopabt 3999 tpexg 4179 3optocl 4418 fun2ssres 4943 funssfv 5199 fvun1 5239 foco2 5318 f1elima 5412 eloprabga 5591 caovimo 5694 ot1stg 5779 ot2ndg 5780 ot3rdgg 5781 brtposg 5869 rdgexggg 5964 rdgivallem 5968 frecsuclem1 5987 nnmass 6066 nndir 6069 nnaword 6084 th3q 6211 ecovass 6215 ecoviass 6216 findcard 6345 addasspig 6428 mulasspig 6430 mulcanpig 6433 ltapig 6436 ltmpig 6437 addassnqg 6480 ltbtwnnqq 6513 mulnnnq0 6548 addassnq0 6560 genpassl 6622 genpassu 6623 genpassg 6624 aptiprleml 6737 adddir 7018 le2tri3i 7126 addsub12 7224 subdir 7383 reapmul1 7586 recexaplem2 7633 div12ap 7673 divdiv32ap 7696 divdivap1 7699 zaddcllemneg 8284 fnn0ind 8354 xrltso 8717 iccgelb 8801 elicc4 8809 elfz 8880 fzrevral 8967 expivallem 9256 expnegap0 9263 expgt0 9288 expge0 9291 expge1 9292 mulexpzap 9295 expp1zap 9303 expm1ap 9304 abssubap0 9686 |
Copyright terms: Public domain | W3C validator |