![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ad4antlr | Structured version Visualization version Unicode version |
Description: Deduction adding 4 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.) |
Ref | Expression |
---|---|
ad2ant.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ad4antlr |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ad2ant.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | ad3antlr 742 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | adantr 471 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
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 190 df-an 377 |
This theorem is referenced by: ad5antlr 746 initoeu2 15959 cpmatacl 19788 cpmatmcllem 19790 cpmatmcl 19791 chfacfisf 19926 chfacfisfcpmat 19927 restcld 20236 pthaus 20701 txhaus 20710 xkohaus 20716 alexsubALTlem4 21113 ustuqtop3 21306 ulmcau 23398 usgra2wlkspth 25397 clwlkisclwwlklem1 25563 usg2spot2nb 25841 locfinreflem 28715 cmpcref 28725 pstmxmet 28748 sigapildsys 29032 ldgenpisyslem1 29033 nn0prpwlem 31026 poimirlem29 32013 heicant 32019 mblfinlem3 32023 mblfinlem4 32024 itg2addnclem2 32038 itg2gt0cn 32041 ftc1cnnc 32060 sstotbnd2 32150 pell1234qrdich 35751 jm2.26lem3 35900 cvgdvgrat 36705 icccncfext 37802 fourierdlem34 38041 fourierdlem87 38094 etransclem35 38171 bgoldbwt 38915 bgoldbtbnd 38941 ply1mulgsumlem2 40451 nn0sumshdiglemA 40702 |
Copyright terms: Public domain | W3C validator |