Theorem baibd 549

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 538	. . 3 ⊢ (𝜒 → (𝜃 ↔ (𝜒 ∧ 𝜃)))
3	2	bicomd 226	. 2 ⊢ (𝜒 → ((𝜒 ∧ 𝜃) ↔ 𝜃))
4	1, 3	sylan9bb 519	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ↔ 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  rbaibd  550  bian1d  591  pw2f1olem  9076  eluz  12892  elicc4  13456  s111  14673  limsupgle  15552  lo1resb  15639  o1resb  15641  isercolllem2  15741  divalgmodcl  16487  ismri2  17710  acsfiel2  17733  eqglact  19291  eqgid  19292  cntzel  19437  dprdsubg  20140  subgdmdprd  20150  dprd2da  20158  dmdprdpr  20165  issubrg3  20749  ishil2  21919  obslbs  21930  iscld2  23235  isperf3  23360  cncnp2  23488  cnnei  23489  trfbas2  24051  flimrest  24191  flfnei  24199  fclsrest  24232  tsmssubm  24351  isnghm2  24932  isnghm3  24933  isnmhm2  24960  iscfil2  25476  caucfil  25493  ellimc2  26087  cnlimc  26098  lhop1  26224  dvfsumlem1  26236  fsumharmonic  27227  fsumvma  27428  fsumvma2  27429  vmasum  27431  chpchtsum  27434  chpub  27435  rpvmasum2  27727  dchrisum0lem1  27731  dirith  27744  uvtx2vtx1edg  29806  uvtx2vtx1edgb  29807  iscplgrnb  29824  frgr3v  30697  adjeu  32312  suppiniseg  33102  suppss3  33138  nndiffz1  33201  indpreima  33255  islinds5  33746  fsumcvg4  34404  qqhval2lem  34435  eulerpartlemf  34825  elorvc  34915  hashreprin  35072  neibastop3  36930  relowlpssretop  38067  sstotbnd2  38483  isbnd3b  38494  lshpkr  39949  isat2  40119  islln4  40339  islpln4  40363  islvol4  40406  islhp2  40829  pw2f1o2val2  43825  modelaxreplem3  45747  rfcnpre1  45797  rfcnpre2  45809  joindm3  49804  meetdm3  49806  catprsc  49848