Theorem jctild 535

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 26	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
3		jctild.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 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:  anc2li  565  equvini  2489  2reu1  3852  frpoinsg  6348  ordunidif  6415  isofrlem  7344  dfwe2  7775  orduniorsuc  7828  tfisg  7852  poxp  8126  fnse  8131  ssenen  9142  dffi3  9394  fpwwe2lem12  10638  zmulcl  12654  rpneg  13061  rexuz3  15419  cau3lem  15425  climrlim2  15617  o1rlimmul  15689  iseralt  15755  gcdzeq  16627  isprm3  16758  vdwnnlem2  17073  chnccat  18699  ablfaclem3  20182  epttop  23195  lmcnp  23490  dfconn2  23605  txcnp  23806  cmphaushmeo  23986  isfild  24044  cnpflf2  24186  flimfnfcls  24214  alexsubALT  24237  fgcfil  25459  bcthlem5  25516  ivthlem2  25640  ivthlem3  25641  dvfsumrlim  26219  plypf1  26398  noetalem1  27934  noseqinds  28515  axeuclidlem  29341  usgr2wlkneq  30134  wwlksnredwwlkn0  30274  wwlksnextwrd  30275  clwlkclwwlklem2a1  30372  lnon0  31179  hstles  32612  mdsl1i  32702  atcveq0  32729  atcvat4i  32778  cdjreui  32813  issgon  34536  onvfowev  35616  connpconn  35740  outsideofrflx  36632  isbasisrelowllem1  38034  isbasisrelowllem2  38035  poimirlem3  38307  poimirlem29  38333  poimir  38337  heicant  38339  equivtotbnd  38462  ismtybndlem  38490  cvrat4  40250  linepsubN  40559  pmapsub  40575  osumcllem4N  40766  pexmidlem1N  40777  dochexmidlem1  42267  cantnfresb  44084  harval3  44297  clcnvlem  44382  relpfrlem  45695  iccpartimp  48199  sbgoldbwt  48575  sbgoldbst  48576  elsetrecslem  50510