Theorem jca2 523

Description: Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 12-Oct-2010.)

Hypotheses

Ref	Expression
jca2.1	⊢ (𝜑 → (𝜓 → 𝜒))
jca2.2	⊢ (𝜓 → 𝜃)

Assertion

Ref	Expression
jca2	⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))

Proof of Theorem jca2

Step	Hyp	Ref	Expression
1		jca2.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		jca2.2	. . 3 ⊢ (𝜓 → 𝜃)
3	2	a1i 11	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
4	1, 3	jcad 522	1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  rr19.28v  3621  preddowncl  6335  ssimaex  6971  onfununi  8353  oaordex  8570  domtriord  9146  findcard3  9278  unfilem1  9301  inf0  9626  inf3lem3  9635  tcel  9748  fidomtri2  10079  alephval3  10193  zorn2lem6  10583  fodomb  10609  eqreznegel  13065  iserodd  17019  cshwsiun  17283  txcn  23951  ssfg  24197  fclsnei  24344  eldmgm  27355  ordunmax  35766  fnrelpredd  35773  cvmlift2lem10  36164  axtco1from2  37356  bj-axreprepsep  38084  pibt2  38434  relcnveq3  39353  iss2  39370  elrelscnveq3  39653  jca3  40007  prjspreln0  43731  omabs2  44428  tfsconcatrn  44438  rfovcnvf1od  45098  mnuop3d  45349  ssclaxsep  46066