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  3622  preddowncl  6334  ssimaex  6968  onfununi  8342  oaordex  8559  domtriord  9135  findcard3  9267  unfilem1  9290  inf0  9615  inf3lem3  9624  tcel  9737  fidomtri2  10068  alephval3  10182  zorn2lem6  10572  fodomb  10598  eqreznegel  13054  iserodd  17006  cshwsiun  17270  txcn  23938  ssfg  24184  fclsnei  24331  eldmgm  27342  fnrelpredd  35709  cvmlift2lem10  36056  axtco1from2  37243  bj-axreprepsep  37971  relcnveq3  39239  iss2  39256  elrelscnveq3  39539  jca3  39893  prjspreln0  43617  omabs2  44318  tfsconcatrn  44328  rfovcnvf1od  44989  mnuop3d  45240  ssclaxsep  45950