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  9079  eluz  12901  elicc4  13466  s111  14683  limsupgle  15564  lo1resb  15651  o1resb  15653  isercolllem2  15753  divalgmodcl  16497  ismri2  17720  acsfiel2  17743  eqglact  19304  eqgid  19305  cntzel  19450  dprdsubg  20153  subgdmdprd  20163  dprd2da  20171  dmdprdpr  20178  issubrg3  20762  ishil2  21932  obslbs  21943  iscld2  23253  isperf3  23378  cncnp2  23506  cnnei  23507  trfbas2  24069  flimrest  24209  flfnei  24217  fclsrest  24250  tsmssubm  24369  isnghm2  24950  isnghm3  24951  isnmhm2  24978  iscfil2  25494  caucfil  25511  ellimc2  26104  cnlimc  26115  lhop1  26241  dvfsumlem1  26253  fsumharmonic  27248  fsumvma  27449  fsumvma2  27450  vmasum  27452  chpchtsum  27455  chpub  27456  rpvmasum2  27748  dchrisum0lem1  27752  dirith  27765  uvtx2vtx1edg  29858  uvtx2vtx1edgb  29859  iscplgrnb  29876  frgr3v  30755  adjeu  32370  suppiniseg  33158  suppss3  33194  nndiffz1  33257  indpreima  33311  islinds5  33802  fsumcvg4  34460  qqhval2lem  34491  eulerpartlemf  34881  elorvc  34971  hashreprin  35128  neibastop3  36981  relowlpssretop  38118  sstotbnd2  38524  isbnd3b  38535  lshpkr  39990  isat2  40160  islln4  40380  islpln4  40404  islvol4  40447  islhp2  40870  pw2f1o2val2  43881  modelaxreplem3  45803  rfcnpre1  45853  rfcnpre2  45865  joindm3  49895  meetdm3  49897  catprsc  49939