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  3773  exmid1stab  4209  trsucss  4424  ordsucim  4500  onsucelsucr  4508  0elnn  4619  xpsspw  4739  relop  4778  fununi  5285  poxp  6233  nntri1  6497  nnsseleq  6502  nnmordi  6517  nnaordex  6529  nnm00  6531  swoord2  6565  nneneq  6857  exmidonfinlem  7192  elni2  7313  prubl  7485  distrlem4prl  7583  distrlem4pru  7584  ltxrlt  8023  recexre  8535  remulext1  8556  mulext1  8569  un0addcl  9209  un0mulcl  9210  elnnz  9263  zleloe  9300  zindd  9371  uzsplit  10092  fzm1  10100  expcl2lemap  10532  expnegzap  10554  expaddzap  10564  expmulzap  10566  qsqeqor  10631  nn0opthd  10702  facdiv  10718  facwordi  10720  bcpasc  10746  recvguniq  11004  absexpzap  11089  maxabslemval  11217  xrmaxiflemval  11258  sumrbdclem  11385  summodc  11391  zsumdc  11392  prodrbdclem  11579  zproddc  11587  prodssdc  11597  fprodcl2lem  11613  fprodsplitsn  11641  ordvdsmul  11841  gcdaddm  11985  lcmdvds  12079  dvdsprime  12122  prmdvdsexpr  12150  prmfac1  12152  pythagtriplem2  12266  unct  12443  baspartn  13553  reopnap  14041  coseq0q4123  14258  lgsdir2lem2  14433  decidin  14552  bj-charfun  14562  bj-nntrans  14706  bj-nnelirr  14708  bj-findis  14734  triap  14780