Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ad5antr | Structured version Visualization version Unicode version |
Description: Deduction adding 5 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Ref | Expression |
---|---|
ad2ant.1 |
Ref | Expression |
---|---|
ad5antr |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ad2ant.1 | . . 3 | |
2 | 1 | ad4antr 768 | . 2 |
3 | 2 | adantr 481 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 |
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 386 |
This theorem is referenced by: ad6antr 772 catass 16347 catpropd 16369 cidpropd 16370 monpropd 16397 funcpropd 16560 fucpropd 16637 drsdirfi 16938 mhmmnd 17537 neitr 20984 xkoccn 21422 trust 22033 restutopopn 22042 ucncn 22089 trcfilu 22098 ulmcau 24149 lgamucov 24764 tgcgrxfr 25413 tgbtwnconn1 25470 legov 25480 legso 25494 midexlem 25587 perpneq 25609 footex 25613 colperpexlem3 25624 colperpex 25625 opphllem 25627 opphllem3 25641 outpasch 25647 hlpasch 25648 lmieu 25676 trgcopy 25696 trgcopyeu 25698 dfcgra2 25721 acopyeu 25725 cgrg3col4 25734 f1otrg 25751 omndmul2 29712 fimaproj 29900 qtophaus 29903 locfinreflem 29907 hgt750lemb 30734 matunitlindflem1 33405 heicant 33444 mblfinlem3 33448 mblfinlem4 33449 itg2gt0cn 33465 sstotbnd2 33573 pell1234qrdich 37425 supxrgelem 39553 icccncfext 40100 etransclem35 40486 smflimlem2 40980 |
Copyright terms: Public domain | W3C validator |