![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ancli | Structured version Visualization version Unicode version |
Description: Deduction conjoining antecedent to left of consequent. (Contributed by NM, 12-Aug-1993.) |
Ref | Expression |
---|---|
ancli.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ancli |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ancli.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | jca 539 |
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: pm4.45im 569 barbari 2407 cesaro 2413 camestros 2414 calemos 2424 swopo 4787 xpdifid 5287 xpima 5301 elrnrexdm 6054 ixpsnf1o 7593 php4 7790 ssnnfi 7822 inf3lem6 8169 rankuni 8365 cardprclem 8444 nqpr 9470 letrp1 10480 p1le 10481 sup2 10598 peano2uz2 11057 uzind 11061 uzid 11207 qreccl 11318 xrsupsslem 11626 supxrunb1 11639 faclbnd4lem4 12519 cshweqdifid 12962 fprodsplit1f 14099 idghm 16953 efgred 17453 srgbinom 17833 subrgid 18065 m1detdiag 19677 1elcpmat 19794 phtpcer 22081 pntrlog2bndlem2 24472 wlkon 25317 trlon 25326 pthon 25361 spthon 25368 constr3lem6 25433 clwwlkf 25578 hvpncan 26748 chsupsn 27122 ssjo 27156 elim2ifim 28217 rrhre 28876 pmeasadd 29208 bnj596 29606 bnj1209 29658 bnj996 29816 bnj1110 29841 bnj1189 29868 arg-ax 31126 bj-mo3OLD 31493 unirep 32085 rp-isfinite6 36209 monoords 37589 fsumsplit1 37736 fmul01 37744 fmuldfeqlem1 37746 fmuldfeq 37747 fmul01lt1lem1 37748 icccncfext 37851 iblspltprt 37936 stoweidlem3 37964 stoweidlem17 37978 stoweidlem19 37980 stoweidlem20 37981 stoweidlem23 37984 stirlinglem15 38051 fourierdlem16 38086 fourierdlem21 38091 fourierdlem72 38143 fourierdlem89 38160 fourierdlem90 38161 fourierdlem91 38162 hoidmvlelem4 38527 zeoALTV 38934 n0rex 39125 c0mgm 40278 c0mhm 40279 2zrngnmrid 40319 mndpsuppss 40525 linc0scn0 40585 |
Copyright terms: Public domain | W3C validator |