Theorem jaod 707

Description: Deduction disjoining the antecedents of two implications. (Contributed by NM, 18-Aug-1994.) (Revised by NM, 4-Apr-2013.)

Hypotheses

Ref	Expression
jaod.1	⊢ (𝜑 → (𝜓 → 𝜒))
jaod.2	⊢ (𝜑 → (𝜃 → 𝜒))

Assertion

Ref	Expression
jaod	⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))

Proof of Theorem jaod

Step	Hyp	Ref	Expression
1		jaod.1	. . . 4 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	com12 30	. . 3 ⊢ (𝜓 → (𝜑 → 𝜒))
3		jaod.2	. . . 4 ⊢ (𝜑 → (𝜃 → 𝜒))
4	3	com12 30	. . 3 ⊢ (𝜃 → (𝜑 → 𝜒))
5	2, 4	jaoi 706	. 2 ⊢ ((𝜓 ∨ 𝜃) → (𝜑 → 𝜒))
6	5	com12 30	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))

Syntax hints:   → wi 4   ∨ wo 698

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpjaod  708  jaao  709  orel2  716  pm2.621  737  mtord  773  jaodan  787  pm2.63  790  pm2.74  797  dedlema  959  dedlemb  960  oplem1  965  opthpr  3752  trsucss  4401  ordsucim  4477  onsucelsucr  4485  0elnn  4596  xpsspw  4716  relop  4754  fununi  5256  poxp  6200  nntri1  6464  nnsseleq  6469  nnmordi  6484  nnaordex  6495  nnm00  6497  swoord2  6531  nneneq  6823  exmidonfinlem  7149  elni2  7255  prubl  7427  distrlem4prl  7525  distrlem4pru  7526  ltxrlt  7964  recexre  8476  remulext1  8497  mulext1  8510  un0addcl  9147  un0mulcl  9148  elnnz  9201  zleloe  9238  zindd  9309  uzsplit  10027  fzm1  10035  expcl2lemap  10467  expnegzap  10489  expaddzap  10499  expmulzap  10501  qsqeqor  10565  nn0opthd  10635  facdiv  10651  facwordi  10653  bcpasc  10679  recvguniq  10937  absexpzap  11022  maxabslemval  11150  xrmaxiflemval  11191  sumrbdclem  11318  summodc  11324  zsumdc  11325  prodrbdclem  11512  zproddc  11520  prodssdc  11530  fprodcl2lem  11546  fprodsplitsn  11574  ordvdsmul  11774  gcdaddm  11917  lcmdvds  12011  dvdsprime  12054  prmdvdsexpr  12082  prmfac1  12084  pythagtriplem2  12198  unct  12375  baspartn  12688  reopnap  13178  coseq0q4123  13395  lgsdir2lem2  13570  decidin  13678  bj-charfun  13689  bj-nntrans  13833  bj-nnelirr  13835  bj-findis  13861  exmid1stab  13880  triap  13908