![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ad3antlr | GIF version |
Description: Deduction adding three conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.) |
Ref | Expression |
---|---|
ad2ant.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
ad3antlr | ⊢ ((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ad2ant.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | ad2antlr 489 | . 2 ⊢ (((𝜒 ∧ 𝜑) ∧ 𝜃) → 𝜓) |
3 | 2 | adantr 276 | 1 ⊢ ((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 |
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 is referenced by: ad4antlr 495 nntr2 6506 phpm 6867 phplem4on 6869 fidifsnen 6872 fisbth 6885 fin0 6887 fin0or 6888 fiintim 6930 fisseneq 6933 djudom 7094 difinfsnlem 7100 nnnninfeq 7128 nnnninfeq2 7129 enomnilem 7138 enmkvlem 7161 enwomnilem 7169 exmidapne 7261 prmuloc 7567 cauappcvgprlemopl 7647 cauappcvgprlemdisj 7652 cauappcvgprlemladdfl 7656 caucvgprlemopl 7670 axcaucvglemcau 7899 xnn0letri 9805 xaddf 9846 xleaddadd 9889 ssfzo12bi 10227 rebtwn2zlemstep 10255 btwnzge0 10302 addmodlteq 10400 frecuzrdgg 10418 qsqeqor 10633 apexp1 10700 hashxp 10808 cjap 10917 caucvgre 10992 minmax 11240 xrminmax 11275 sumeq2 11369 fsumconst 11464 ntrivcvgap 11558 prodeq2 11567 p1modz1 11803 bezoutlemmain 12001 dfgcd2 12017 uzwodc 12040 lcmgcdlem 12079 mulgval 12991 cnpnei 13758 cnntr 13764 txmetcnp 14057 lgsval 14444 pw1nct 14791 peano4nninf 14794 |
Copyright terms: Public domain | W3C validator |