Theorem jaao 472

Description: Inference conjoining and disjoining the antecedents of two implications.

Hypotheses

Ref	Expression
jaao.1	|- (ph -> (ps -> ch))
jaao.2	|- (th -> (ta -> ch))

Assertion

Ref	Expression
jaao	|- ((ph /\ th) -> ((ps \/ ta) -> ch))

Proof of Theorem jaao

Step	Hyp	Ref	Expression
1		jaao.1	. . 3 |- (ph -> (ps -> ch))
2	1	adantr 425	. 2 |- ((ph /\ th) -> (ps -> ch))
3		jaao.2	. . 3 |- (th -> (ta -> ch))
4	3	adantl 424	. 2 |- ((ph /\ th) -> (ta -> ch))
5	2, 4	jaod 469	1 |- ((ph /\ th) -> ((ps \/ ta) -> ch))

Syntax hints:   -> wi 3   \/ wo 239   /\ wa 240

This theorem is referenced by:  3jaaoOLD 1165  prssOLD 3139  fr2nr 3635  ordtri1 3693  ordtri1OLD 3694  ordun 3771  suc11 3773  funun 4462  suc11reg 5710  abslti 8127  abslei 8128  unctb 8846  gcdcllem2 13719  gcdcllem3 13720  poxp 13949  fprod1ib 14686  ralunOLD 15657

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

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242

Copyright terms: Public domain