Theorem jaod 717

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 716	. 2 ⊢ ((𝜓 ∨ 𝜃) → (𝜑 → 𝜒))
6	5	com12 30	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))

Syntax hints:   → wi 4   ∨ wo 708

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 709

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjaod  718  jaao  719  orel2  726  pm2.621  747  mtord  783  jaodan  797  pm2.63  800  pm2.74  807  dedlema  969  dedlemb  970  oplem1  975  opthpr  3771  exmid1stab  4206  trsucss  4421  ordsucim  4497  onsucelsucr  4505  0elnn  4616  xpsspw  4736  relop  4774  fununi  5281  poxp  6228  nntri1  6492  nnsseleq  6497  nnmordi  6512  nnaordex  6524  nnm00  6526  swoord2  6560  nneneq  6852  exmidonfinlem  7187  elni2  7308  prubl  7480  distrlem4prl  7578  distrlem4pru  7579  ltxrlt  8017  recexre  8529  remulext1  8550  mulext1  8563  un0addcl  9203  un0mulcl  9204  elnnz  9257  zleloe  9294  zindd  9365  uzsplit  10085  fzm1  10093  expcl2lemap  10525  expnegzap  10547  expaddzap  10557  expmulzap  10559  qsqeqor  10623  nn0opthd  10693  facdiv  10709  facwordi  10711  bcpasc  10737  recvguniq  10995  absexpzap  11080  maxabslemval  11208  xrmaxiflemval  11249  sumrbdclem  11376  summodc  11382  zsumdc  11383  prodrbdclem  11570  zproddc  11578  prodssdc  11588  fprodcl2lem  11604  fprodsplitsn  11632  ordvdsmul  11832  gcdaddm  11975  lcmdvds  12069  dvdsprime  12112  prmdvdsexpr  12140  prmfac1  12142  pythagtriplem2  12256  unct  12433  baspartn  13330  reopnap  13820  coseq0q4123  14037  lgsdir2lem2  14212  decidin  14320  bj-charfun  14330  bj-nntrans  14474  bj-nnelirr  14476  bj-findis  14502  triap  14548