Theorem baibd 539

Description: Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)

Hypothesis

Ref	Expression
baibd.1	⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))

Assertion

Ref	Expression
baibd	⊢ ((𝜑 ∧ 𝜒) → (𝜓 ↔ 𝜃))

Proof of Theorem baibd

Step	Hyp	Ref	Expression
1		baibd.1	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))
2		ibar 528	. . 3 ⊢ (𝜒 → (𝜃 ↔ (𝜒 ∧ 𝜃)))
3	2	bicomd 223	. 2 ⊢ (𝜒 → ((𝜒 ∧ 𝜃) ↔ 𝜃))
4	1, 3	sylan9bb 509	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  rbaibd  540  pw2f1olem  9022  eluz  12783  elicc4  13350  s111  14556  limsupgle  15419  lo1resb  15506  o1resb  15508  isercolllem2  15608  divalgmodcl  16353  ismri2  17569  acsfiel2  17592  eqglact  19087  eqgid  19088  cntzel  19231  dprdsubg  19932  subgdmdprd  19942  dprd2da  19950  dmdprdpr  19957  issubrg3  20485  ishil2  21604  obslbs  21615  iscld2  22891  isperf3  23016  cncnp2  23144  cnnei  23145  trfbas2  23706  flimrest  23846  flfnei  23854  fclsrest  23887  tsmssubm  24006  isnghm2  24588  isnghm3  24589  isnmhm2  24616  iscfil2  25142  caucfil  25159  ellimc2  25754  cnlimc  25765  lhop1  25895  dvfsumlem1  25908  fsumharmonic  26898  fsumvma  27100  fsumvma2  27101  vmasum  27103  chpchtsum  27106  chpub  27107  rpvmasum2  27399  dchrisum0lem1  27403  dirith  27416  uvtx2vtx1edg  29301  uvtx2vtx1edgb  29302  iscplgrnb  29319  frgr3v  30177  adjeu  31791  suppiniseg  32582  suppss3  32620  nndiffz1  32682  indpreima  32761  islinds5  33311  fsumcvg4  33913  qqhval2lem  33944  eulerpartlemf  34334  elorvc  34424  hashreprin  34584  neibastop3  36323  relowlpssretop  37325  sstotbnd2  37741  isbnd3b  37752  lshpkr  39083  isat2  39253  islln4  39474  islpln4  39498  islvol4  39541  islhp2  39964  pw2f1o2val2  43002  modelaxreplem3  44943  rfcnpre1  44986  rfcnpre2  44998  joindm3  48930  meetdm3  48932  catprsc  48975