![]() |
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 481 | . 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓) |
3 | 2 | ad4antr 730 | 1 ⊢ ((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 206 df-an 397 |
This theorem is referenced by: ad6antr 734 ad6antlr 735 simp-5l 783 fimaproj 8063 catass 17558 catpropd 17581 cidpropd 17582 monpropd 17612 funcpropd 17779 fucpropd 17858 drsdirfi 18186 mhmmnd 18860 neitr 22515 xkoccn 22954 trust 23565 restutopopn 23574 ucncn 23621 trcfilu 23630 ulmcau 25738 lgamucov 26371 tgcgrxfr 27346 tgbtwnconn1 27403 legov 27413 legso 27427 midexlem 27520 perpneq 27542 footexALT 27546 footex 27549 colperpexlem3 27560 colperpex 27561 opphllem 27563 opphllem3 27577 outpasch 27583 hlpasch 27584 lmieu 27612 trgcopy 27632 trgcopyeu 27634 dfcgra2 27658 acopyeu 27662 cgrg3col4 27681 f1otrg 27699 fnpreimac 31473 nn0xmulclb 31559 s3f1 31686 omndmul2 31803 cyc3conja 31889 nsgqusf1olem3 32076 rhmimaidl 32085 mxidlprm 32116 ssmxidllem 32117 fedgmul 32203 extdg1id 32229 qtophaus 32286 locfinreflem 32290 zarclssn 32323 hgt750lemb 33138 matunitlindflem1 36041 heicant 36080 mblfinlem3 36084 mblfinlem4 36085 itg2gt0cn 36100 sstotbnd2 36200 aks4d1p8 40511 aks6d1c2p2 40516 fsuppind 40703 pell1234qrdich 41122 omabs2 41603 supxrgelem 43507 icccncfext 44060 etransclem35 44442 smflimlem2 44945 |
Copyright terms: Public domain | W3C validator |