Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mpbir2an | Unicode version |
Description: Detach a conjunction of truths in a biconditional. (Contributed by NM, 10-May-2005.) (Revised by NM, 9-Jan-2015.) |
Ref | Expression |
---|---|
mpbir2an.1 | |
mpbir2an.2 | |
mpbiran2an.1 |
Ref | Expression |
---|---|
mpbir2an |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpbir2an.2 | . 2 | |
2 | mpbir2an.1 | . . 3 | |
3 | mpbiran2an.1 | . . 3 | |
4 | 2, 3 | mpbiran 935 | . 2 |
5 | 1, 4 | mpbir 145 | 1 |
Colors of variables: wff set class |
Syntax hints: wa 103 wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: 3pm3.2i 1170 euequ1 2114 eqssi 3163 elini 3311 dtruarb 4177 opnzi 4220 so0 4311 we0 4346 ord0 4376 ordon 4470 onsucelsucexmidlem1 4512 regexmidlemm 4516 ordpwsucexmid 4554 reg3exmidlemwe 4563 ordom 4591 funi 5230 funcnvsn 5243 funinsn 5247 fnresi 5315 fn0 5317 f0 5388 fconst 5393 f10 5476 f1o0 5479 f1oi 5480 f1osn 5482 isoid 5789 iso0 5796 acexmidlem2 5850 fo1st 6136 fo2nd 6137 iordsmo 6276 tfrlem7 6296 tfrexlem 6313 mapsnf1o2 6674 1domsn 6797 inresflem 7037 0ct 7084 infnninf 7100 infnninfOLD 7101 exmidonfinlem 7170 exmidaclem 7185 pw1on 7203 sucpw1nel3 7210 1pi 7277 prarloclemcalc 7464 ltsopr 7558 ltsosr 7726 cnm 7794 axicn 7825 axaddf 7830 axmulf 7831 nnindnn 7855 ltso 7997 negiso 8871 nnind 8894 0z 9223 dfuzi 9322 cnref1o 9609 elrpii 9613 xrltso 9753 0e0icopnf 9936 0e0iccpnf 9937 fz0to4untppr 10080 fldiv4p1lem1div2 10261 expcl2lemap 10488 expclzaplem 10500 expge0 10512 expge1 10513 xrnegiso 11225 fclim 11257 eff2 11643 reeff1 11663 ef01bndlem 11719 sin01bnd 11720 cos01bnd 11721 sin01gt0 11724 egt2lt3 11742 halfleoddlt 11853 2prm 12081 3prm 12082 1arith 12319 setsslnid 12467 fntopon 12816 istpsi 12831 ismeti 13140 tgqioo 13341 addcncntoplem 13345 divcnap 13349 abscncf 13366 recncf 13367 imcncf 13368 cjcncf 13369 dveflem 13481 reeff1o 13488 reefiso 13492 ioocosf1o 13569 lgslem2 13696 lgsfcl2 13701 lgsne0 13733 ex-fl 13760 bj-indint 13966 bj-omord 13995 012of 14028 2o01f 14029 0nninf 14037 peano4nninf 14039 taupi 14102 |
Copyright terms: Public domain | W3C validator |