Theorem jctild 533

Description: Deduction conjoining a theorem to left of consequent in an implication. (Contributed by NM, 21-Apr-2005.)

Hypotheses

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

Assertion

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

Proof of Theorem jctild

Step	Hyp	Ref	Expression
1		jctild.2	. . 3 ⊢ (𝜑 → 𝜃)
2	1	a1d 25	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
3		jctild.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 3	jcad 520	1 ⊢ (𝜑 → (𝜓 → (𝜃 ∧ 𝜒)))

Syntax hints:   → wi 4   ∧ wa 399

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

This theorem depends on definitions:  df-bi 209  df-an 400

This theorem is referenced by:  anc2li  563  equvini  2485  2reu1  3848  frpoinsg  6325  ordunidif  6391  isofrlem  7319  dfwe2  7752  orduniorsuc  7805  tfisg  7829  poxp  8102  fnse  8107  ssenen  9117  dffi3  9371  fpwwe2lem12  10594  zmulcl  12614  rpneg  13021  rexuz3  15367  cau3lem  15373  climrlim2  15565  o1rlimmul  15637  iseralt  15703  gcdzeq  16577  isprm3  16708  vdwnnlem2  17023  chnccat  18649  ablfaclem3  20120  epttop  23057  lmcnp  23352  dfconn2  23467  txcnp  23668  cmphaushmeo  23848  isfild  23906  cnpflf2  24048  flimfnfcls  24076  alexsubALT  24099  fgcfil  25321  bcthlem5  25378  ivthlem2  25502  ivthlem3  25503  dvfsumrlim  26081  plypf1  26260  noetalem1  27793  noseqinds  28374  axeuclidlem  29120  usgr2wlkneq  29913  wwlksnredwwlkn0  30053  wwlksnextwrd  30054  clwlkclwwlklem2a1  30151  lnon0  30958  hstles  32391  mdsl1i  32481  atcveq0  32508  atcvat4i  32557  cdjreui  32592  issgon  34381  onvfowev  35420  connpconn  35546  outsideofrflx  36438  isbasisrelowllem1  37810  isbasisrelowllem2  37811  poimirlem3  38083  poimirlem29  38109  poimir  38113  heicant  38115  equivtotbnd  38238  ismtybndlem  38266  cvrat4  40028  linepsubN  40337  pmapsub  40353  osumcllem4N  40544  pexmidlem1N  40555  dochexmidlem1  42045  cantnfresb  43862  harval3  44075  clcnvlem  44160  relpfrlem  45490  iccpartimp  47984  sbgoldbwt  48360  sbgoldbst  48361  elsetrecslem  50281