Theorem jaod 329

Description: Deduction disjoining the antecedents of two implications.

Hypotheses

Ref	Expression
jaod.1	⊢ (φ → (ψ → χ))
jaod.2	⊢ (φ → (θ → χ))

Assertion

Ref	Expression
jaod	⊢ (φ → ((ψ ∨ θ) → χ))

Proof of Theorem jaod

Step	Hyp	Ref	Expression
1		jao 274	. 2 ⊢ ((ψ → χ) → ((θ → χ) → ((ψ ∨ θ) → χ)))
2		jaod.1	. 2 ⊢ (φ → (ψ → χ))
3		jaod.2	. 2 ⊢ (φ → (θ → χ))
4	1, 2, 3	sylc 62	1 ⊢ (φ → ((ψ ∨ θ) → χ))

Syntax hints:   → wi 2   ∨ wo 195

This theorem is referenced by:  jaao 330  ccased 563  dedlema 569  dedlemb 570  psssstr 1576  sotric 2148  ordtr2 2257  trsucss 2309  limom 2387  fununi 2705  tfrlem11 2959  oaass 3163  omordi 3164  omsmolem 3195  mapdom2 3389  nneneq 3408  inf3lem6 3469  r1ord3 3501  zornlem7 3609  cardnn 3631  carddom 3642  sucdom 3648  unxpdomlem 3649  alephordi 3679  cardaleph 3690  cfsuc 3709  indpi 3828  ltrpq 3879  prub 3892  sqgt0sr 4009  ssgt0sr 4011  suppsr3 4018  lelttrt 4289  ltletrt 4290  letrt 4291  nn2get 4438  nnleltp1t 4448  nnsub 4450  sup2 4510  lt0nnn0 4549  elnnz 4572  nn0subt 4587  nn0opth 4724  sqrlem6 4736  sqrlem12 4742  infxpidmlem7 4939  infdif 4948  atcvat 5771

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198

metamath.org