New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > mpgbir | Unicode version |
Description: Modus ponens on biconditional combined with generalization. (Contributed by NM, 24-May-1994.) (Proof shortened by Stefan Allan, 28-Oct-2008.) |
Ref | Expression |
---|---|
mpgbir.1 | |
mpgbir.2 |
Ref | Expression |
---|---|
mpgbir |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpgbir.2 | . . 3 | |
2 | 1 | ax-gen 1546 | . 2 |
3 | mpgbir.1 | . 2 | |
4 | 2, 3 | mpbir 200 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wb 176 wal 1540 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 |
This theorem depends on definitions: df-bi 177 |
This theorem is referenced by: nfi 1551 cvjust 2348 eqriv 2350 abbi2i 2464 nfci 2479 abid2f 2514 rgen 2679 ssriv 3277 ss2abi 3338 ssmin 3945 intab 3956 iunab 4012 iinab 4027 nincompl 4072 peano1 4402 addcnul1 4452 ncvspfin 4538 xpvv 4843 relssi 4848 eqrelriv 4850 eqoprriv 4853 dm0 4918 dmi 4919 co01 5093 ssdmrn 5099 funopabeq 5140 funsn 5147 fvopab3ig 5387 1stfo 5505 2ndfo 5506 swapf1o 5511 dmep 5524 caovmo 5645 fnfullfunlem2 5857 fvfullfunlem3 5863 clos1is 5881 |
Copyright terms: Public domain | W3C validator |