New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > mpbird | Unicode version |
Description: A deduction from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
mpbird.min | |
mpbird.maj |
Ref | Expression |
---|---|
mpbird |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpbird.min | . 2 | |
2 | mpbird.maj | . . 3 | |
3 | 2 | biimprd 214 | . 2 |
4 | 1, 3 | mpd 14 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 176 |
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 177 |
This theorem is referenced by: mpbiri 224 mpbir2and 888 mpbir3and 1135 eqeltrd 2427 eqnetrd 2534 3netr4d 2543 eqsstrd 3305 3sstr4d 3314 lefinaddc 4450 nulge 4456 ltfinp1 4462 tfinprop 4489 sucevenodd 4510 sucoddeven 4511 sfintfin 4532 eqbrtrd 4659 3brtr4d 4669 eqfnfvd 5395 fvimacnvi 5402 fconst2g 5452 f1ofveu 5480 f1od 5726 brtxp 5783 trrd 5925 refrd 5926 antird 5928 connexrd 5930 iserd 5942 enmap2lem5 6067 enmap1lem5 6073 enprmaplem5 6080 nenpw1pwlem2 6085 pw1eltc 6162 ce0nnuli 6178 ce0 6190 lecidg 6196 lec0cg 6198 lecncvg 6199 addlec 6208 nmembers1lem3 6270 spacis 6288 nchoicelem17 6305 dmfrec 6316 frec0 6321 frecsuc 6322 |
Copyright terms: Public domain | W3C validator |