Theorem impel 505

Description: An inference for implication elimination. (Contributed by Giovanni Mascellani, 23-May-2019.) (Proof shortened by Wolf Lammen, 2-Sep-2020.)

Hypotheses

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

Assertion

Ref	Expression
impel	⊢ ((𝜑 ∧ 𝜃) → 𝜒)

Proof of Theorem impel

Step	Hyp	Ref	Expression
1		impel.2	. . 3 ⊢ (𝜃 → 𝜓)
2		impel.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5 34	. 2 ⊢ (𝜑 → (𝜃 → 𝜒))
4	3	imp 406	1 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  equs5e  2463  mob2  3675  ssn0rex  4312  reusv2lem2  5346  copsex2t  5448  reuop  6259  trssord  6342  trsuc  6414  funimass2  6583  fvelima  6907  fvmptf  6971  funfvima2  7187  funfvima3  7192  tfi  7805  suppssov1  8149  suppssov2  8150  tposf2  8202  frrlem4  8241  ectocld  8731  mapsnd  8836  resixpfo  8886  f1oeng  8919  nneneq  9142  fodomfi  9224  fiint  9239  fodomfiOLD  9242  eqinf  9400  hartogslem1  9459  cantnf  9614  rankwflemb  9717  carden2a  9890  carduni  9905  harval2  9921  cardaleph  10011  alephval3  10032  dfac5  10051  cfcof  10196  axdc4lem  10377  nqereu  10852  recexsr  11030  seqcoll  14399  swrdswrd  14640  swrdccatin1  14660  swrdccatin2  14664  repswswrd  14719  climcau  15606  odd2np1  16280  lcmfunsnlem2lem2  16578  coprmproddvdslem  16601  dvdsprm  16642  vdwlem6  16926  imasvscafn  17470  dirref  18536  irredn1  20374  isdrngd  20710  isdrngdOLD  20712  psgnghm  21547  gsummoncoe1  22264  prdstopn  23584  cnextcn  24023  tnggrpr  24611  ovolctb  25459  dyadmbl  25569  itg1addlem4  25668  itg1le  25682  dvcnp2  25889  dvcnp2OLD  25890  c1liplem1  25969  pserulm  26399  fsumdvdsmul  27173  perfectlem2  27209  dchrisumlem2  27469  noresle  27677  bday1  27822  readdscl  28507  remulscl  28510  axlowdimlem16  29042  wlkv0  29735  wlkp1lem1  29757  wlkswwlksf1o  29964  wspniunwspnon  30008  trlsegvdeglem1  30307  frcond4  30357  2clwwlk2clwwlk  30437  opabssi  32702  nn0xmulclb  32861  zarclsiin  34048  rankval4b  35275  cusgr3cyclex  35349  satfun  35624  fundmpss  35980  nn0prpw  36536  bj-restpw  37342  bj-prmoore  37365  cgsex2gd  37389  domalom  37656  cover2  37963  disjlem18  39151  sticksstones11  42523  setindtr  43378  onov0suclim  43628  oe0suclim  43631  ofoaid1  43712  ofoaid2  43713  naddcnfcom  43720  naddcnfass  43723  omssaxinf2  45341  climxlim2lem  46200  sge0f1o  46737  2reuimp  47472  fvelsetpreimafv  47744  imasetpreimafvbijlemfo  47762  reupr  47879  lighneallem4  47967  proththd  47971  lincresunit3  48838  oppc1stflem  49643