Theorem ifboth 4528

Description: A wff 𝜃 containing a conditional operator is true when both of its cases are true. (Contributed by NM, 3-Sep-2006.) (Revised by Mario Carneiro, 15-Feb-2015.)

Hypotheses

Ref	Expression
ifboth.1	⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜃))
ifboth.2	⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜃))

Assertion

Ref	Expression
ifboth	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem ifboth

Step	Hyp	Ref	Expression
1		ifboth.1	. 2 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝜓 ↔ 𝜃))
2		ifboth.2	. 2 ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝜒 ↔ 𝜃))
3		simpll 766	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜑) → 𝜓)
4		simplr 768	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ ¬ 𝜑) → 𝜒)
5	1, 2, 3, 4	ifbothda 4527	1 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  ifcif 4488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-if 4489

This theorem is referenced by:  ifcl  4534  keephyp  4560  soltmin  6109  xrmaxlt  13141  xrltmin  13142  xrmaxle  13143  xrlemin  13144  ifle  13157  expmulnbnd  14200  limsupgre  15447  isumless  15811  cvgrat  15849  rpnnen2lem4  16185  ruclem2  16200  sadcaddlem  16427  sadadd3  16431  pcmptdvds  16865  prmreclem5  16891  prmreclem6  16892  pnfnei  23107  mnfnei  23108  xkopt  23542  xmetrtri2  24244  stdbdxmet  24403  stdbdmet  24404  stdbdmopn  24406  xrsxmet  24698  icccmplem2  24712  metdscn  24745  metnrmlem1a  24747  ivthlem2  25353  ovolicc2lem5  25422  ioombl1lem1  25459  ioombl1lem4  25462  ismbfd  25540  mbfi1fseqlem4  25619  mbfi1fseqlem5  25620  itg2const  25641  itg2const2  25642  itg2monolem3  25653  itg2gt0  25661  itg2cnlem1  25662  itg2cnlem2  25663  iblss  25706  itgless  25718  ibladdlem  25721  iblabsr  25731  iblmulc2  25732  bddiblnc  25743  dvferm1lem  25888  dvferm2lem  25890  dvlip2  25900  dgradd2  26174  plydiveu  26206  chtppilim  27386  dchrvmasumiflem1  27412  ostth3  27549  1smat1  33794  poimirlem24  37638  mblfinlem2  37652  itg2addnclem  37665  itg2addnc  37668  itg2gt0cn  37669  ibladdnclem  37670  iblmulc2nc  37679  ftc1anclem5  37691  ftc1anclem8  37694  ftc1anc  37695