![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ad5antr | Structured version Visualization version GIF version |
Description: Deduction adding 5 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.) |
Ref | Expression |
---|---|
ad2ant.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
ad5antr | ⊢ ((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ad2ant.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | adantr 480 | . 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓) |
3 | 2 | ad4antr 769 | 1 ⊢ ((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 197 df-an 385 |
This theorem is referenced by: ad6antr 777 ad6antrOLD 778 ad6antlr 779 catass 16394 catpropd 16416 cidpropd 16417 monpropd 16444 funcpropd 16607 fucpropd 16684 drsdirfi 16985 mhmmnd 17584 neitr 21032 xkoccn 21470 trust 22080 restutopopn 22089 ucncn 22136 trcfilu 22145 ulmcau 24194 lgamucov 24809 tgcgrxfr 25458 tgbtwnconn1 25515 legov 25525 legso 25539 midexlem 25632 perpneq 25654 footex 25658 colperpexlem3 25669 colperpex 25670 opphllem 25672 opphllem3 25686 outpasch 25692 hlpasch 25693 lmieu 25721 trgcopy 25741 trgcopyeu 25743 dfcgra2 25766 acopyeu 25770 cgrg3col4 25779 f1otrg 25796 omndmul2 29840 fimaproj 30028 qtophaus 30031 locfinreflem 30035 hgt750lemb 30862 matunitlindflem1 33535 heicant 33574 mblfinlem3 33578 mblfinlem4 33579 itg2gt0cn 33595 sstotbnd2 33703 pell1234qrdich 37742 supxrgelem 39866 icccncfext 40418 etransclem35 40804 smflimlem2 41301 |
Copyright terms: Public domain | W3C validator |