Theorem jaod 722

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

Syntax hints:   → wi 4   ∨ wo 713

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 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjaod  723  jaao  724  orel2  731  pm2.621  752  mtord  788  jaodan  802  pm2.63  805  pm2.74  812  dedlema  975  dedlemb  976  oplem1  981  ifnebibdc  3648  opthpr  3849  exmid1stab  4291  trsucss  4513  ordsucim  4591  onsucelsucr  4599  0elnn  4710  xpsspw  4830  relop  4871  fununi  5388  poxp  6376  nntri1  6640  nnsseleq  6645  nnmordi  6660  nnaordex  6672  nnm00  6674  swoord2  6708  nneneq  7014  exmidonfinlem  7367  elni2  7497  prubl  7669  distrlem4prl  7767  distrlem4pru  7768  ltxrlt  8208  recexre  8721  remulext1  8742  mulext1  8755  un0addcl  9398  un0mulcl  9399  elnnz  9452  zleloe  9489  zindd  9561  uzsplit  10284  fzm1  10292  expcl2lemap  10768  expnegzap  10790  expaddzap  10800  expmulzap  10802  qsqeqor  10867  nn0opthd  10939  facdiv  10955  facwordi  10957  bcpasc  10983  recvguniq  11501  absexpzap  11586  maxabslemval  11714  xrmaxiflemval  11756  sumrbdclem  11883  summodc  11889  zsumdc  11890  prodrbdclem  12077  zproddc  12085  prodssdc  12095  fprodcl2lem  12111  fprodsplitsn  12139  ordvdsmul  12340  gcdaddm  12500  nninfctlemfo  12556  lcmdvds  12596  dvdsprime  12639  prmdvdsexpr  12667  prmfac1  12669  pythagtriplem2  12784  4sqlem11  12919  unct  13008  domneq0  14230  baspartn  14718  reopnap  15214  coseq0q4123  15502  lgsdir2lem2  15702  upgrpredgv  15938  decidin  16119  bj-charfun  16128  bj-nntrans  16272  bj-nnelirr  16274  bj-findis  16300  triap  16356