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  bian1d  580  pw2f1olem  9013  eluz  12796  elicc4  13360  s111  14572  limsupgle  15433  lo1resb  15520  o1resb  15522  isercolllem2  15622  divalgmodcl  16370  ismri2  17592  acsfiel2  17615  eqglact  19148  eqgid  19149  cntzel  19292  dprdsubg  19995  subgdmdprd  20005  dprd2da  20013  dmdprdpr  20020  issubrg3  20571  ishil2  21712  obslbs  21723  iscld2  23006  isperf3  23131  cncnp2  23259  cnnei  23260  trfbas2  23821  flimrest  23961  flfnei  23969  fclsrest  24002  tsmssubm  24121  isnghm2  24702  isnghm3  24703  isnmhm2  24730  iscfil2  25246  caucfil  25263  ellimc2  25857  cnlimc  25868  lhop1  25994  dvfsumlem1  26006  fsumharmonic  26992  fsumvma  27193  fsumvma2  27194  vmasum  27196  chpchtsum  27199  chpub  27200  rpvmasum2  27492  dchrisum0lem1  27496  dirith  27509  uvtx2vtx1edg  29484  uvtx2vtx1edgb  29485  iscplgrnb  29502  frgr3v  30363  adjeu  31978  suppiniseg  32777  suppss3  32814  nndiffz1  32877  indpreima  32943  islinds5  33445  fsumcvg4  34113  qqhval2lem  34144  eulerpartlemf  34533  elorvc  34623  hashreprin  34783  neibastop3  36563  relowlpssretop  37697  sstotbnd2  38112  isbnd3b  38123  lshpkr  39580  isat2  39750  islln4  39970  islpln4  39994  islvol4  40037  islhp2  40460  pw2f1o2val2  43489  modelaxreplem3  45428  rfcnpre1  45471  rfcnpre2  45483  joindm3  49459  meetdm3  49461  catprsc  49503