MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpbi2and Structured version   Visualization version   GIF version

Theorem mpbi2and 957
Description: Detach a conjunction of truths in a biconditional. (Contributed by NM, 6-Nov-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
Hypotheses
Ref Expression
mpbi2and.1 (𝜑𝜓)
mpbi2and.2 (𝜑𝜒)
mpbi2and.3 (𝜑 → ((𝜓𝜒) ↔ 𝜃))
Assertion
Ref Expression
mpbi2and (𝜑𝜃)

Proof of Theorem mpbi2and
StepHypRef Expression
1 mpbi2and.1 . . 3 (𝜑𝜓)
2 mpbi2and.2 . . 3 (𝜑𝜒)
31, 2jca 552 . 2 (𝜑 → (𝜓𝜒))
4 mpbi2and.3 . 2 (𝜑 → ((𝜓𝜒) ↔ 𝜃))
53, 4mpbid 220 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382
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 195  df-an 384
This theorem is referenced by:  supiso  8238  hartogslem1  8304  cantnfp1lem3  8434  oemapwe  8448  cantnffval2  8449  mulne0d  10525  flflp1  12422  flval2  12429  remim  13648  ntrivcvgtail  14414  divalgmod  14910  divalgmodOLD  14911  divnumden  15237  numdensq  15243  prmdivdiv  15273  4sqlem7  15429  isposd  16721  latasymd  16823  latjidm  16840  latmidm  16852  latledi  16855  latjass  16861  mod1ile  16871  isglbd  16883  lubun  16889  poslubmo  16912  posglbmo  16913  ismgmid2  17033  oppginv  17555  slwhash  17805  lsmmod  17854  iscmnd  17971  dprd2da  18207  dmdprdsplit2lem  18210  dprdsplit  18213  pgpfac1lem1  18239  imasring  18385  isdrngd  18538  subrg1  18556  lsmsp  18850  lspprabs  18859  lsmcv  18905  psr1  19176  mat1  20011  topgele  20488  lmcn2  21201  dvdsq1p  23638  wilthlem2  24509  dchr1  24696  ismir  25269  atcvatlem  28431  ressprs  28789  rngurd  28922  ordtconlem1  29101  cvmliftphtlem  30356  cvmlift3lem6  30363  cvmlift3lem9  30366  poimirlem13  32392  poimirlem14  32393  lsatexch  33148  lsatcvatlem  33154  oldmm1  33322  olj01  33330  olm01  33341  cvrcmp  33388  atcvreq0  33419  cvlexchb1  33435  cvlcvr1  33444  exatleN  33508  hlrelat3  33516  cvrval3  33517  cvratlem  33525  atlelt  33542  cvrat3  33546  2atjm  33549  atbtwn  33550  hlatexch3N  33584  hlatexch4  33585  2llnmat  33628  2atm  33631  lplnexllnN  33668  2llnjaN  33670  4atlem11b  33712  4atlem12b  33715  2lplnja  33723  dalem1  33763  dalemcea  33764  dalem3  33768  dalem8  33774  dalem16  33783  dalem17  33784  dalem21  33798  dalem25  33802  dalem39  33815  dalem54  33830  dalem55  33831  dalem57  33833  dalem60  33836  2lnat  33888  2atm2atN  33889  2llnma1b  33890  cdlema1N  33895  paddasslem12  33935  paddasslem13  33936  pmodlem1  33950  dalawlem2  33976  dalawlem3  33977  dalawlem5  33979  dalawlem6  33980  dalawlem8  33982  dalawlem11  33985  dalawlem12  33986  osumcllem1N  34060  lhp2lt  34105  lhpexle2lem  34113  lhpexle3lem  34115  lhpocnle  34120  lhpat3  34150  4atexlemtlw  34171  4atexlemnclw  34174  4atexlemcnd  34176  lautj  34197  lautm  34198  trlval3  34292  cdlemc5  34300  cdlemd3  34305  cdleme3g  34339  cdleme3h  34340  cdleme7d  34351  cdleme11c  34366  cdleme11k  34373  cdleme15d  34382  cdleme16e  34387  cdleme16f  34388  cdleme17b  34392  cdlemednpq  34404  cdleme19a  34409  cdleme20j  34424  cdleme21c  34433  cdleme22aa  34445  cdleme22b  34447  cdleme22cN  34448  cdleme22d  34449  cdleme23c  34457  cdleme28a  34476  cdleme35a  34554  cdleme35b  34556  cdleme35f  34560  cdleme42i  34589  cdlemeg46req  34635  cdlemf2  34668  cdlemg4c  34718  cdlemg6c  34726  cdlemg8b  34734  cdlemg10  34747  cdlemg11b  34748  cdlemg12f  34754  cdlemg13a  34757  cdlemg17a  34767  cdlemg17dALTN  34770  cdlemg18b  34785  cdlemg19a  34789  cdlemg27a  34798  cdlemg33b0  34807  cdlemg35  34819  cdlemg42  34835  cdlemg46  34841  trljco  34846  tendopltp  34886  cdlemi  34926  cdlemk3  34939  cdlemk10  34949  cdlemk15  34961  cdlemk1u  34965  cdlemk39  35022  cdlemk50  35058  erng1lem  35093  erngdvlem4  35097  erngdvlem4-rN  35105  dialss  35153  dia2dimlem1  35171  dia2dimlem10  35180  dia2dimlem12  35182  cdlemm10N  35225  djajN  35244  diblss  35277  cdlemn2  35302  dihjustlem  35323  dihord1  35325  dihord2pre2  35333  dib2dim  35350  dih2dimb  35351  dih2dimbALTN  35352  dihopelvalcpre  35355  dihord5b  35366  dihord5apre  35369  dihmeetlem1N  35397  dihglblem5apreN  35398  dihglblem2N  35401  dihmeetlem2N  35406  dihmeetlem3N  35412  lclkrlem2f  35619  lclkrlem2v  35635  lclkrslem2  35645  lcfrlem25  35674  lcfrlem35  35684  mapdlsm  35771  fourierdlem54  38854  fourierdlem76  38876  vdgfrgrgt2  41467
  Copyright terms: Public domain W3C validator