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 480 | . 2 ⊢ (((𝜒 ∧ 𝜑) ∧ 𝜃) → 𝜓) |
3 | 2 | adantr 274 | 1 ⊢ ((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem is referenced by: ad4antlr 486 nntr2 6367 phpm 6727 phplem4on 6729 fidifsnen 6732 fisbth 6745 fin0 6747 fin0or 6748 fiintim 6785 fisseneq 6788 djudom 6946 difinfsnlem 6952 enomnilem 6978 prmuloc 7342 cauappcvgprlemopl 7422 cauappcvgprlemdisj 7427 cauappcvgprlemladdfl 7431 caucvgprlemopl 7445 axcaucvglemcau 7674 xaddf 9595 xleaddadd 9638 ssfzo12bi 9970 rebtwn2zlemstep 9998 btwnzge0 10041 addmodlteq 10139 frecuzrdgg 10157 hashxp 10540 cjap 10646 caucvgre 10721 minmax 10969 xrminmax 11002 sumeq2 11096 fsumconst 11191 bezoutlemmain 11613 dfgcd2 11629 lcmgcdlem 11685 cnpnei 12315 cnntr 12321 txmetcnp 12614 peano4nninf 13127 nninfalllemn 13129 |
Copyright terms: Public domain | W3C validator |