Theorem orbi12d 805

Description: Deduction joining two equivalences to form equivalence of disjunctions. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
orbi12d.1	|- ( ph -> ( ps <-> ch ) )
orbi12d.2	|- ( ph -> ( th <-> ta ) )

Assertion

Ref	Expression
orbi12d	|- ( ph -> ( ( ps \/ th ) <-> ( ch \/ ta ) ) )

Proof of Theorem orbi12d

Step	Hyp	Ref	Expression
1		orbi12d.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	orbi1d 803	. 2 |- ( ph -> ( ( ps \/ th ) <-> ( ch \/ th ) ) )
3		orbi12d.2	. . 3 |- ( ph -> ( th <-> ta ) )
4	3	orbi2d 802	. 2 |- ( ph -> ( ( ch \/ th ) <-> ( ch \/ ta ) ) )
5	2, 4	bitrd 188	1 |- ( ph -> ( ( ps \/ th ) <-> ( ch \/ ta ) ) )

Syntax hints:   -> wi 4   <-> wb 105   \/ wo 720

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm4.39  834  dcbid  850  ifpbi123d  1005  3orbi123d  1352  dfbi3dc  1446  eueq3dc  3000  sbcor  3096  sbcorg  3097  unjust  3223  elun  3370  elif  3649  ifbi  3658  elprg  3725  eltpg  3750  rabsnifsb  3773  rabrsndc  3775  preq12bg  3893  exmid01  4330  exmidsssnc  4335  swopolem  4445  soeq1  4455  sowlin  4460  ordtri2orexmid  4665  regexmidlemm  4674  regexmidlem1  4675  reg2exmidlema  4676  ordsoexmid  4704  ordtri2or2exmid  4713  ontri2orexmidim  4714  nn0suc  4746  nndceq0  4760  0elnn  4761  soinxp  4840  fununi  5444  funcnvuni  5445  fun11iun  5655  unpreima  5824  isosolem  6020  xporderlem  6457  poxp  6458  frec0g  6658  freccllem  6663  frecfcllem  6665  frecsuclem  6667  frecsuc  6668  inffiexmid  7203  fidcenumlemrk  7261  isomni  7466  enomnilem  7468  finomni  7470  exmidomni  7472  fodjuomnilemres  7478  onntri45  7590  papeq1  7599  papcotr  7603  tapeq1  7608  netap  7610  2omotaplemap  7613  indpi  7699  ltexprlemloc  7964  addextpr  7978  ltsosr  8121  aptisr  8136  mulextsr1lem  8137  mulextsr1  8138  axpre-ltwlin  8240  axpre-apti  8242  axpre-mulext  8245  axltwlin  8383  axapti  8386  axsuploc  8388  reapval  8894  reapti  8897  reapmul1lem  8912  reapmul1  8913  reapadd1  8914  reapneg  8915  reapcotr  8916  remulext1  8917  apreim  8921  apsym  8924  apcotr  8925  apadd1  8926  addext  8928  apneg  8929  nn1m1nn  9301  nn1gt1  9317  elznn0  9638  elz2  9695  nn0n0n1ge2b  9704  nneoor  9727  uztric  9923  ltxr  10156  fzsplit2  10433  fzsplit3  10436  uzsplit  10477  nelfzo  10537  fzospliti  10563  fzouzsplit  10566  exbtwnzlemstep  10660  exbtwnzlemex  10662  qavgle  10671  frec2uzled  10844  sq11ap  11123  swrdnd  11409  sqrt11ap  11782  abs00ap  11806  maxclpr  11966  minmax  11974  minclpr  11981  xrmaxiflemcom  11993  xrminmax  12009  xrminltinf  12016  sumeq1  12099  sumeq2  12103  fz1f1o  12119  summodc  12128  fsum3  12132  prodeq1f  12297  prodeq2w  12301  prodeq2  12302  prodmodc  12323  fprodseq  12328  fprodcl2lem  12350  zeo3  12613  odd2np1lem  12617  dvdsprime  12878  coprm  12900  ennnfonelemrnh  13285  gzsumvalx  13686  gzsumfzval  13688  gzsumress  13689  gzsum0  13690  islring  14472  opprlring  14477  isdomn  14551  opprdomnbg  14556  znidom  14964  reopnap  15570  dich0  15676  reapef  15802  logrpap0b  15900  wilthlem1  16008  perfectlem2  16028  lgslem1  16033  upgrm  16255  upgr1or2  16256  upgr1elem1  16275  edgupgren  16296  usgruspgrben  16341  subupgr  16428  konigsberglem1  16643  dichmul0orlem3  16669  dichmul0orlem7  16673  decidi  16737  bj-nn0suc0  16890  bj-inf2vnlem2  16911  bj-nn0sucALT  16918  isomninnlem  16984  trilpolemlt1  16995  trirec0  16998